(*Note that, hypothesis are properties need to prove. After closing the section, they will turn to the hypothesis of a formula. 
Axiom are properties that need not be proved.*)

Require Import Omega.
Require Import Arith.
Require Import Classical.

Lemma my_proof_irrelevance_lr : forall (p1 p2 : Prop), (p1 = p2) -> (p1 <-> p2).
intros.
rewrite H;tauto.
Qed.

Axiom my_proof_irrelevance_rl : forall (p1 p2 : Prop), (p1 <-> p2) -> (p1 = p2).

Ltac elim_clear H := elim H;intros;clear H.
Ltac g_intro H := generalize H;intros.

(*the following three defintions are for the concrete model*)
Definition Position := nat.
Definition Var_c := Position -> Prop.
Definition Time_c := nat.

(*the following three defintions are for the abstact model*)
Definition Cycle := nat.
Definition Var := Cycle -> Prop.
Definition Time := nat.

(*the quiz mechine concrete model*)

(*l0 is for the i/o phase, each one of the others represents one rung*)
Inductive location : Set := 
l0 | l1 | l2 | l3 | l4 | l5 | l6 | l7 | l8 | l9 | l10.

Definition program_counter := Position -> location.

(*help notations*)

Definition being_true_c (v : Var_c) (p1 p2 : Position) (l : location) (pc : program_counter):= 
                           forall p, p1 <= p <= p2 -> pc p = l -> v p.

Definition being_false_c (v : Var_c) (p1 p2 : Position) (l : location) (pc : program_counter):= 
                           forall p, p1 <= p <= p2 -> pc p = l -> ~ v p.


Print being_false_c.

(*
all the relays without timer
i0 - start
i1 - reset
i2 - player 1
i3 - player 2
i4 - player 3

m1 - running symbol
m2 - player 1
m3 - player 2
m4 - player 3
m5 - lock symbol if any one press the button

o0 - time out
o1 - player 1 pressed
o2 - player 2 pressed
o3 - player 3 pressed

*)
Variables i0 i1 i2 i3 i4 : Var_c.
Variables m1 m2 m3 m4 m5: Var_c.
Variables o0 o1 o2 o3 : Var_c.

Variable t1 : Var_c.
Variable t1_PT_c : Time_c.
Hypothesis t1_PT_c_gt_zero : 1 <= t1_PT_c.

Variable pc : program_counter.

Variable fc : Position -> Time_c.
Hypothesis fc_monotonic : forall p, fc p < fc (S p).

Lemma fc_monotonic_g : forall p1 p2, p1 < p2 -> fc p1 < fc p2.
induction 1.
apply fc_monotonic.
generalize (fc_monotonic m);intros.
omega.
Qed.

Lemma fc_monotonic_gr : forall p1 p2, fc p1 < fc p2 -> p1 < p2.
intros.
cut (p1 < p2 \/ p2 <= p1);[|try omega];intros.
elim_clear H0;auto.
SearchPattern (_ < _ \/ _).
elim (le_lt_or_eq _ _ H1);intros.
generalize (fc_monotonic_g _ _ H0);intros;omega.
rewrite H0 in H.
omega.
Qed.


(*initial valuation*)

Definition initial_condition_c i0 i1 i2 i3 i4 m1 m2 m3 m4 m5 o0 o1 o2 o3 pc t1:=
    i0 = False /\ i1 = False /\ i2 = False /\ i3 = False /\ i4 = False /\
    m1 = False /\ m2 = False /\ m3 = False /\ m4 = False /\ m5 = False /\
    o0 = False /\ o1= False /\ o2 = False /\ o3= False /\
    pc = l0 /\ t1 = False.

Check initial_condition_c.

Definition next_condition_c (i0 i1 i2 i3 i4 m1 m2 m3 m4 m5 o0 o1 o2 o3:Prop) l (t1 i0' i1' i2' i3' i4' m1' m2' m3' m4' m5' o0' o1' o2' o3':Prop) l' t1':= 
    match l with 
            l0 => m1' = m1 /\ m2' = m2 /\ m3' = m3 /\ m4' = m4 /\ m5' = m5 /\ 
                     o0' = o0 /\ o1' = o1 /\ o2' = o2 /\ o3' = o3 /\
                     t1' = t1 /\
                     l' = l1
            | l1 => m1' = ((m1 \/ i0) /\ (~ i1)) /\
                     i0' = i0 /\ i1' = i1 /\ i2' = i2 /\ i3' = i3 /\ i4' = i4 /\ 
                     m2' = m2 /\ m3' = m3 /\ m4' = m4 /\ m5' = m5 /\ 
                     o0' = o0 /\ o1' = o1 /\ o2' = o2 /\ o3' = o3 /\
                     t1' = t1 /\
                     l' = l2
            | l2 => i0' = i0 /\ i1' = i1 /\ i2' = i2 /\ i3' = i3 /\ i4' = i4 /\ 
                     m1' = m1 /\ m2' = m2 /\ m3' = m3 /\ m4' = m4 /\ m5' = m5 /\ 
                     o0' = o0 /\ o1' = o1 /\ o2' = o2 /\ o3' = o3 /\
                     l' = l3
            |l3 => m2' = ((m2 \/ (~t1 /\ i2 /\ ~ m5)) /\ m1) /\  
                     i0' = i0 /\ i1' = i1 /\ i2' = i2 /\ i3' = i3 /\ i4' = i4 /\ 
                     m1' = m1 /\ m3' = m3 /\ m4' = m4 /\ m5' = m5 /\ 
                     o0' = o0 /\ o1' = o1 /\ o2' = o2 /\ o3' = o3 /\
                     t1' = t1 /\
                     l' = l4
            |l4 => m3' = ((m3 \/ (~t1 /\ i3 /\ ~ m5)) /\ m1) /\
                     i0' = i0 /\ i1' = i1 /\ i2' = i2 /\ i3' = i3 /\ i4' = i4 /\ 
                     m1' = m1 /\ m2' = m2 /\ m4' = m4 /\ m5' = m5 /\ 
                     o0' = o0 /\ o1' = o1 /\ o2' = o2 /\ o3' = o3 /\
                     t1' = t1 /\
                     l' =l5
            |l5 => m4' = ((m4 \/ (~t1 /\ i4 /\ ~ m5)) /\ m1) /\
                     i0' = i0 /\ i1' = i1 /\ i2' = i2 /\ i3' = i3 /\ i4' = i4 /\ 
                     m1' = m1 /\ m2' = m2 /\ m3' = m3 /\ m5' = m5 /\ 
                     o0' = o0 /\ o1' = o1 /\ o2' = o2 /\ o3' = o3 /\
                     t1' = t1 /\
                     l' =l6
            |l6 => m5' = ((m2 \/ m3 \/ m4 \/ m5) /\ m1) /\
                     i0' = i0 /\ i1' = i1 /\ i2' = i2 /\ i3' = i3 /\ i4' = i4 /\ 
                     m1' = m1 /\ m2' = m2 /\ m3' = m3 /\ m4' = m4 /\ 
                     o0' = o0 /\ o1' = o1 /\ o2' = o2 /\ o3' = o3 /\
                     t1' = t1 /\
                     l' =l7
            |l7 => o1' = m2 /\ 
                     i0' = i0 /\ i1' = i1 /\ i2' = i2 /\ i3' = i3 /\ i4' = i4 /\ 
                     m1' = m1 /\ m2' = m2 /\ m3' = m3 /\ m4' = m4 /\ m5' = m5 /\ 
                     o0' = o0 /\ o2' = o2 /\ o3' = o3 /\
                     t1' = t1 /\
                     l' =l8
            |l8 => o2' = m3 /\
                     i0' = i0 /\ i1' = i1 /\ i2' = i2 /\ i3' = i3 /\ i4' = i4 /\ 
                     m1' = m1 /\ m2' = m2 /\ m3' = m3 /\ m4' = m4 /\ m5' = m5 /\ 
                     o0' = o0 /\ o1' = o1 /\ o3' = o3 /\
                     t1' = t1 /\
                     l' =l9
            |l9 => o3' = m4 /\
                     i0' = i0 /\ i1' = i1 /\ i2' = i2 /\ i3' = i3 /\ i4' = i4 /\ 
                     m1' = m1 /\ m2' = m2 /\ m3' = m3 /\ m4' = m4 /\ m5' = m5 /\ 
                     o0' = o0 /\ o1' = o1 /\ o2' = o2 /\ 
                     t1' = t1 /\
                     l' =l10
            |l10 => o0' = (t1 /\ ~ m5) /\
                     i0' = i0 /\ i1' = i1 /\ i2' = i2 /\ i3' = i3 /\ i4' = i4 /\ 
                     m1' = m1 /\ m2' = m2 /\ m3' = m3 /\ m4' = m4 /\ m5' = m5 /\ 
                     o1' = o1 /\ o2' = o2 /\ o3' = o3 /\
                     t1' = t1 /\
                     l' =l0
    end.

Print next_condition_c.


Hypothesis INIT_c : initial_condition_c  (i0 0) (i1 0) (i2 0) (i3 0) (i4 0) (m1 0) (m2 0) (m3 0) (m4 0) (m5 0) (o0 0) (o1 0) (o2 0) (o3 0) (pc 0) (t1 0).
Hypothesis NEXT_c : forall p, 
    next_condition_c (i0 p) (i1 p) (i2 p) (i3 p) (i4 p) (m1 p) (m2 p) (m3 p) (m4 p) (m5 p) (o0 p) (o1 p) (o2 p) (o3 p) (pc p) (t1 p)
    (i0 (S p)) (i1 (S p)) (i2 (S p)) (i3 (S p)) (i4 (S p)) (m1 (S p)) (m2 (S p)) (m3 (S p)) (m4 (S p)) (m5 (S p)) (o0 (S p)) (o1 (S p)) (o2 (S p)) (o3 (S p)) (pc (S p)) (t1 (S p)).

(*concrete model of a more detailed TON-timer*)

Hypothesis h_t1_reset_c : forall p, pc p = l2 -> ~ m1 p -> ~ t1 (S p).
Hypothesis h_t1_set_c : forall p1 p2, pc p1 = l2 -> pc p2 = l2 -> 
                                                                t1_PT_c <= fc p2 - fc p1 ->
                                                                being_true_c m1 p1 p2 l2 pc ->
                                                                t1 (S p2). 
Hypothesis h_t1_true_c : forall p2, pc (pred p2) = l2 -> t1 p2 -> 
                                                                exists p1, pc p1 = l2 /\ t1_PT_c <= fc (pred p2) - fc p1 /\
                                                                                  being_true_c m1 p1 (pred p2) l2 pc.

Print h_t1_reset_c.
Print h_t1_set_c.
Print h_t1_true_c.

(*mapping from the concrete model to the abstact model, and its properties*)

Variable f_mapping : nat -> Position.

Hypothesis f_mapping_before_0 : forall p, p < f_mapping 0 -> ~ pc p =  l0.
Hypothesis f_mapping_point_to_l0 : forall n, pc (f_mapping n) =  l0.
Hypothesis f_mapping_no_l0_between : forall n1 n2 p, f_mapping n1 < p < f_mapping n2 -> ~ pc p = l0. 
(*Hypothesis from_abs_to_con_4 : forall n1 n2, n1 <> n2 -> f_mapping n1 <> f_mapping n2.*)
Hypothesis f_mapping_monotony : forall n1 n2, n1 < n2 -> f_mapping n1 < f_mapping n2.

(*this used the structure of the concrete model*)
Lemma f_mapping_0_0 : f_mapping 0 = 0.
SearchPattern (_ > 0 \/ _).
elim (gt_O_eq (f_mapping 0));intros;auto.
generalize (f_mapping_before_0 0);intros.
generalize INIT_c;intros.
red in H1.
intuition.
Qed.

Lemma f_mapping_larger : forall p, p <= f_mapping p.
induction p.
rewrite f_mapping_0_0;auto.
assert (f_mapping p < f_mapping (S p));intros.
apply f_mapping_monotony;omega.
omega.
Qed.

Lemma f_mapping_between : forall p, exists n, f_mapping n <= p <= f_mapping (S n).
induction p.
exists 0.
split;auto with arith.
rewrite f_mapping_0_0;auto.
elim IHp;intros.
elim_clear H;intros.
SearchPattern (_ < _ \/ _).
elim (le_lt_or_eq _ _ H1);intros.
exists x;omega.
exists (S x);split.
rewrite H.
auto with arith.
assert (f_mapping(S x) < f_mapping (S (S x))).
apply f_mapping_monotony;auto with arith.
omega.
Qed.

Lemma f_mapping_le : forall n1 n2, n1 <= n2 -> f_mapping n1 <= f_mapping n2.
induction 1;auto.
generalize (f_mapping_monotony m (S m));omega.
Qed.

Lemma f_mapping_gr : forall n1 n2, f_mapping n1 <= f_mapping n2 -> n1 <= n2.
intros.
cut (n1 < n2 \/ n2 <= n1);[|try omega];intros.
elim_clear H0;auto with arith.
SearchPattern (_ < _ \/ _).
elim (le_lt_or_eq _ _ H1);intros.
generalize (f_mapping_monotony _ _ H0);intros;omega.
rewrite H0 in H.
omega.
Qed.


Lemma f_mapping_next_unique : 
        forall n1 p1 p2, p1 < p2 -> f_mapping n1 = p1 -> 
              pc p1 = l0 -> pc p2 = l0 -> (forall p, p1 < p < p2 -> pc p <> l0) -> 
                         f_mapping (S n1) = p2.
intros.
cut (f_mapping (S n1) <= p1 \/ p1 < f_mapping (S n1) /\ f_mapping (S n1) < p2 \/ p2 <= f_mapping (S n1));try omega.
intros.
elim_clear H4.
rewrite <- H0 in H5.
generalize (f_mapping_monotony n1 (S n1));intros.
apply False_ind.
omega.
elim_clear H5.
apply False_ind.
generalize (f_mapping_point_to_l0);intros.
red in H3.
eapply H3.
apply H4.
auto.
elim (le_lt_or_eq p2 (f_mapping (S n1)));intros;auto.
generalize (f_mapping_no_l0_between n1 (S n1));intros.
apply False_ind.
red in H6.
eapply H6.
cut (f_mapping n1 < p2 < f_mapping (S n1));intros.
apply H7.
omega.
auto.
Qed.

Hint Resolve f_mapping_before_0 f_mapping_point_to_l0 f_mapping_no_l0_between f_mapping_monotony f_mapping_next_unique f_mapping_0_0 : base_f_mapping.

(*abstract traces*)
Definition abs (T:Type) (v : Position -> T) (f_mapping : nat ->Position) (n:nat):= v (f_mapping n).
Implicit Arguments abs [T]. 

Check abs.

Print abs.
Check (abs m1 f_mapping).

(*end of the model*)

Hint Resolve INIT_c : transition_hint.

(*the following lemmas tell that given a location, which is the previous location*)

Lemma before_l0_is_l10_or_l0 : forall p, pc p = l0 -> pc (pred p) = l0 \/ pc (pred p)= l10.
intros.
destruct p;simpl.
left;auto with transition_hint.
right;generalize (NEXT_c p);intro H_tc;red in H_tc.
destruct (pc p);intuition; try rewrite H in H16; try discriminate H16.
rewrite H in H11;discriminate.
rewrite H in H15;discriminate.
Qed.

Lemma before_l1_is_l0 : forall p, pc p = l1 -> pc (pred p) = l0.
intros.
destruct p;simpl.
generalize (INIT_c);intro H_tc;red in H_tc;tauto.
generalize (NEXT_c p);intro H_tc;red in H_tc.
destruct (pc p);intuition; try rewrite H in H16; try discriminate.
rewrite H in H15;discriminate.
Qed.

Lemma before_l2_is_l1 : forall p, pc p = l2 -> pc (pred p) = l1.
intros.
destruct p;simpl.
generalize (INIT_c);intro H_tc;red in H_tc;intuition.
rewrite H in H14; discriminate.
generalize (NEXT_c p);intro H_tc;red in H_tc.
destruct (pc p);intuition; try rewrite H in H16; try discriminate.
rewrite H in H11;discriminate.
rewrite H in H15;discriminate.
Qed.

Lemma before_l3_is_l2 : forall p, pc p = l3 -> pc (pred p) = l2.
destruct p;simpl.
generalize (INIT_c);intro H_tc;red in H_tc;intuition.
rewrite H in H14; discriminate.
generalize (NEXT_c p);intro H_tc;red in H_tc.
destruct (pc p);intuition; try rewrite H in H16; try discriminate.
rewrite H in H11;discriminate.
Qed.

Lemma before_l4_is_l3 : forall p, pc p = l4 -> pc (pred p) = l3.
destruct p;simpl.
generalize (INIT_c);intro H_tc;red in H_tc;intuition.
rewrite H in H14; discriminate.
generalize (NEXT_c p);intro H_tc;red in H_tc.
destruct (pc p);intuition; try rewrite H in H16; try discriminate.
rewrite H in H11;discriminate.
rewrite H in H15;discriminate.
Qed.

Lemma before_l5_is_l4 : forall p, pc p = l5 -> pc (pred p) = l4.
destruct p;simpl.
generalize (INIT_c);intro H_tc;red in H_tc;intuition.
rewrite H in H14; discriminate.
generalize (NEXT_c p);intro H_tc;red in H_tc.
destruct (pc p);intuition; try rewrite H in H16; try discriminate.
rewrite H in H11;discriminate.
rewrite H in H15;discriminate.
Qed.

Lemma before_l6_is_l5 : forall p, pc p = l6 -> pc (pred p) = l5.
destruct p;simpl.
generalize (INIT_c);intro H_tc;red in H_tc;intuition.
rewrite H in H14; discriminate.
generalize (NEXT_c p);intro H_tc;red in H_tc.
destruct (pc p);intuition; try rewrite H in H16; try discriminate.
rewrite H in H11;discriminate.
rewrite H in H15;discriminate.
Qed.

Lemma before_l7_is_l6 : forall p, pc p = l7 -> pc (pred p) = l6.
destruct p;simpl.
generalize (INIT_c);intro H_tc;red in H_tc;intuition.
rewrite H in H14; discriminate.
generalize (NEXT_c p);intro H_tc;red in H_tc.
destruct (pc p);intuition; try rewrite H in H16; try discriminate.
rewrite H in H11;discriminate.
rewrite H in H15;discriminate.
Qed.

Lemma before_l8_is_l7 : forall p, pc p = l8 -> pc (pred p) = l7.
destruct p;simpl.
generalize (INIT_c);intro H_tc;red in H_tc;intuition.
rewrite H in H14; discriminate.
generalize (NEXT_c p);intro H_tc;red in H_tc.
destruct (pc p);intuition; try rewrite H in H16; try discriminate.
rewrite H in H11;discriminate.
rewrite H in H15;discriminate.
Qed.

Lemma before_l9_is_l8 : forall p, pc p = l9 -> pc (pred p) = l8.
destruct p;simpl.
generalize (INIT_c);intro H_tc;red in H_tc;intuition.
rewrite H in H14; discriminate.
generalize (NEXT_c p);intro H_tc;red in H_tc.
destruct (pc p);intuition; try rewrite H in H16; try discriminate.
rewrite H in H11;discriminate.
rewrite H in H15;discriminate.
Qed.

Lemma before_l10_is_l9 : forall p, pc p = l10 -> pc (pred p) = l9.
destruct p;simpl.
generalize (INIT_c);intro H_tc;red in H_tc;intuition.
rewrite H in H14; discriminate.
generalize (NEXT_c p);intro H_tc;red in H_tc.
destruct (pc p);intuition; try rewrite H in H16; try discriminate.
rewrite H in H11;discriminate.
rewrite H in H15;discriminate.
Qed.

Lemma l0_before_l0_0 : forall p, pc p = l0 -> pc (pred p) = l0 -> p = 0.
intros.
destruct p;simpl in *;auto.
generalize (NEXT_c p);intro H_tc;red in H_tc.
destruct (pc p);intuition; try rewrite H in H12; try discriminate.
Qed.

Lemma before_l0_S_p_is_l10 : forall p, pc (S p) = l0 -> pc p = l10.
intros.
elim (before_l0_is_l10_or_l0 (S p));simpl;intros;auto.
generalize (NEXT_c p);intro Hn;red in Hn.
rewrite H0 in Hn.
intuition.
rewrite H12 in H;discriminate.
Qed.

Lemma l1_lt_1 : forall p, pc p = l1 -> 1 <= p.
intros.
destruct p.
generalize (INIT_c); intro Hi; red in Hi; intuition.
rewrite H14 in H;discriminate.
omega.
Qed.

Lemma l0_between_l0_is_10 : forall p0 p1, p0 < p1 -> pc p0 = l0 -> pc p1 = l0 -> 
                                                                  (forall p, p0 < p < p1-> pc p <> l0) ->  p1 = 11 + p0.
intros.
generalize (NEXT_c p0).
unfold next_condition_c;rewrite H0;simpl.
intros [trans0 [trans1 [trans2 [trans3 [trans4 [trans5 [trans6 [trans7 [trans8 [trans9 trans_0]]]]]]]]]];clear trans0 trans1 trans2 trans3 trans4  trans5 trans6 trans7 trans8 trans9.
generalize (NEXT_c (S p0));unfold next_condition_c;rewrite trans_0;simpl.
intros [trans0 [trans1 [trans2 [trans3 [trans4 [trans5 [trans6 [trans7 [trans8 [trans9 [trans10 [trans11 [trans12 [trans13 [trans14 trans_1]]]]]]]]]]]]]]].
clear trans0 trans1 trans2 trans3 trans4  trans5 trans6 trans7 trans8 trans9 trans10 trans11 trans12 trans13 trans14.
generalize (NEXT_c (S (S p0)));unfold next_condition_c;rewrite trans_1;simpl.
intros [trans0 [trans1 [trans2 [trans3 [trans4 [trans5 [trans6 [trans7 [trans8 [trans9 [trans10 [trans11 [trans12 [trans13 trans_2]]]]]]]]]]]]]].
clear trans0 trans1 trans2 trans3 trans4  trans5 trans6 trans7 trans8 trans9 trans10 trans11 trans12 trans13.
generalize (NEXT_c (S (S (S p0))));unfold next_condition_c;rewrite trans_2;simpl.
intros [trans0 [trans1 [trans2 [trans3 [trans4 [trans5 [trans6 [trans7 [trans8 [trans9 [trans10 [trans11 [trans12 [trans13 [trans14 trans_3]]]]]]]]]]]]]]].
clear trans0 trans1 trans2 trans3 trans4  trans5 trans6 trans7 trans8 trans9 trans10 trans11 trans12 trans13 trans14.
generalize (NEXT_c (S (S (S (S p0)))));unfold next_condition_c;rewrite trans_3;simpl.
intros [trans0 [trans1 [trans2 [trans3 [trans4 [trans5 [trans6 [trans7 [trans8 [trans9 [trans10 [trans11 [trans12 [trans13 [trans14 trans_4]]]]]]]]]]]]]]].
clear trans0 trans1 trans2 trans3 trans4  trans5 trans6 trans7 trans8 trans9 trans10 trans11 trans12 trans13 trans14.
generalize (NEXT_c (S (S (S (S (S p0))))));unfold next_condition_c;rewrite trans_4;simpl.
intros [trans0 [trans1 [trans2 [trans3 [trans4 [trans5 [trans6 [trans7 [trans8 [trans9 [trans10 [trans11 [trans12 [trans13 [trans14 trans_5]]]]]]]]]]]]]]].
clear trans0 trans1 trans2 trans3 trans4  trans5 trans6 trans7 trans8 trans9 trans10 trans11 trans12 trans13 trans14.
generalize (NEXT_c (S (S (S (S (S (S p0)))))));unfold next_condition_c;rewrite trans_5;simpl.
intros [trans0 [trans1 [trans2 [trans3 [trans4 [trans5 [trans6 [trans7 [trans8 [trans9 [trans10 [trans11 [trans12 [trans13 [trans14 trans_6]]]]]]]]]]]]]]].
clear trans0 trans1 trans2 trans3 trans4  trans5 trans6 trans7 trans8 trans9 trans10 trans11 trans12 trans13 trans14.
generalize (NEXT_c (S (S (S (S (S (S (S p0))))))));unfold next_condition_c;rewrite trans_6;simpl.
intros [trans0 [trans1 [trans2 [trans3 [trans4 [trans5 [trans6 [trans7 [trans8 [trans9 [trans10 [trans11 [trans12 [trans13 [trans14 trans_7]]]]]]]]]]]]]]].
clear trans0 trans1 trans2 trans3 trans4  trans5 trans6 trans7 trans8 trans9 trans10 trans11 trans12 trans13 trans14.
generalize (NEXT_c (S (S (S (S (S (S (S (S p0)))))))));unfold next_condition_c;rewrite trans_7;simpl.
intros [trans0 [trans1 [trans2 [trans3 [trans4 [trans5 [trans6 [trans7 [trans8 [trans9 [trans10 [trans11 [trans12 [trans13 [trans14 trans_8]]]]]]]]]]]]]]].
clear trans0 trans1 trans2 trans3 trans4  trans5 trans6 trans7 trans8 trans9 trans10 trans11 trans12 trans13 trans14.
generalize (NEXT_c (S (S (S (S (S (S (S (S (S p0))))))))));unfold next_condition_c;rewrite trans_8;simpl.
intros [trans0 [trans1 [trans2 [trans3 [trans4 [trans5 [trans6 [trans7 [trans8 [trans9 [trans10 [trans11 [trans12 [trans13 [trans14 trans_9]]]]]]]]]]]]]]].
clear trans0 trans1 trans2 trans3 trans4  trans5 trans6 trans7 trans8 trans9 trans10 trans11 trans12 trans13 trans14.
generalize (NEXT_c (S (S (S (S (S (S (S (S (S (S p0)))))))))));unfold next_condition_c;rewrite trans_9;simpl.
intros [trans0 [trans1 [trans2 [trans3 [trans4 [trans5 [trans6 [trans7 [trans8 [trans9 [trans10 [trans11 [trans12 [trans13 [trans14 trans_10]]]]]]]]]]]]]]].
clear trans0 trans1 trans2 trans3 trans4  trans5 trans6 trans7 trans8 trans9 trans10 trans11 trans12 trans13 trans14.
assert (S (S (S (S (S (S (S (S (S (S (S p0)))))))))) = (11 + p0) );auto.
rewrite H3 in *;clear H3.
assert (p1 <= p0 \/ p1 = 1 + p0  \/ p1 = 2 + p0  \/ p1 = 3 + p0  \/ p1 = 4 + p0  \/ p1 = 5 + p0  \/ p1 = 6 + p0  \/ 
              p1 = 7 + p0  \/ p1 = 8 + p0  \/ p1 = 9 + p0  \/ p1 = 10 + p0  \/ p1 = 11 + p0 \/ 11 + p0 < p1).
omega.
simpl in H3.
intuition.
rewrite H3 in H1.
rewrite H1 in trans_0.
discriminate.
rewrite H4 in H1.
rewrite H1 in trans_1.
discriminate.
rewrite H3 in H1.
rewrite H1 in trans_2.
discriminate.
rewrite H4 in H1.
rewrite H1 in trans_3.
discriminate.
rewrite H3 in H1.
rewrite H1 in trans_4.
discriminate.
rewrite H4 in H1.
rewrite H1 in trans_5.
discriminate.
rewrite H3 in H1.
rewrite H1 in trans_6.
discriminate.
rewrite H4 in H1.
rewrite H1 in trans_7.
discriminate.
rewrite H3 in H1.
rewrite H1 in trans_8.
discriminate.
rewrite H4 in H1.
rewrite H1 in trans_9.
discriminate.
simpl in *.
elim (H2 (11+p0));simpl;try omega;auto.
Qed.

Lemma l0_add_1_l1 : forall p, pc p = l0 -> pc (1 + p) = l1.
intros.
generalize (NEXT_c p);rewrite H;simpl;intuition.
Qed.

Lemma l0_add_2_l2 : forall p, pc p = l0 -> pc (2 + p) = l2.
intros.
generalize (l0_add_1_l1 p H);intros Ht.
generalize (NEXT_c (1+ p));rewrite Ht;simpl;intuition.
Qed.

Lemma l0_add_3_l3 : forall p, pc p = l0 -> pc (3 + p) = l3.
intros.
generalize (l0_add_2_l2 p H);intros Ht.
generalize (NEXT_c (2+ p));rewrite Ht;simpl;intuition.
Qed.

Lemma l0_add_4_l4 : forall p, pc p = l0 -> pc (4+ p) = l4.
intros.
generalize (l0_add_3_l3 p H);intros Ht.
generalize (NEXT_c (3+  p));rewrite Ht;simpl;intuition.
Qed.

Lemma l0_add_5_l5 : forall p, pc p = l0 -> pc (5+ p) = l5.
intros.
generalize (l0_add_4_l4 p H);intros Ht.
generalize (NEXT_c (4+  p));rewrite Ht;simpl;intuition.
Qed.

Lemma l0_add_6_l6 : forall p, pc p = l0 -> pc (6+ p) = l6.
intros.
generalize (l0_add_5_l5 p H);intros Ht.
generalize (NEXT_c (5+  p));rewrite Ht;simpl;intuition.
Qed.

Lemma l0_add_7_l7 : forall p, pc p = l0 -> pc (7+ p) = l7.
intros.
generalize (l0_add_6_l6 p H);intros Ht.
generalize (NEXT_c (6+  p));rewrite Ht;simpl;intuition.
Qed.

Lemma l0_add_8_l8 : forall p, pc p = l0 -> pc (8+ p) = l8.
intros.
generalize (l0_add_7_l7 p H);intros Ht.
generalize (NEXT_c (7+  p));rewrite Ht;simpl;intuition.
Qed.

Lemma l0_add_9_l9 : forall p, pc p = l0 -> pc (9+ p) = l9.
intros.
generalize (l0_add_8_l8 p H);intros Ht.
generalize (NEXT_c (8+  p));rewrite Ht;simpl;intuition.
Qed.

Lemma l0_add_10_l10 : forall p, pc p = l0 -> pc (10+ p) = l10.
intros.
generalize (l0_add_9_l9 p H);intros Ht.
generalize (NEXT_c (9+  p));rewrite Ht;simpl;intuition.
Qed.

Lemma l0_add_11_l0 : forall p, pc p = l0 -> pc (11+ p) = l0.
intros.
generalize (l0_add_10_l10 p H);intros Ht.
generalize (NEXT_c (10+  p));rewrite Ht;simpl;intuition.
Qed.

(*be careful when unfold these two definitions.
These two definitions cannot be used for proving purpose.*)
Definition offset := 2.
Definition t1_loc := l2.

(*hypothesis need to be proved based on the concrete model. They are written as hypothesis here. 
name: h_set_1
*)
Lemma t1_loc_change_property : forall n p1 p2, p1 = f_mapping n -> p2 = f_mapping (S n) -> 
                                                            (forall p, p1 <= p < p2 -> pc p <>  t1_loc -> t1 (S p) = t1 p).
unfold t1_loc.
intros.
generalize (NEXT_c p).
destruct (pc p);simpl;intros;intuition.
Qed.

Implicit Arguments t1_loc_change_property [n p1 p2].

Lemma offset_is_t1_loc : forall n p1 p2, p1 = f_mapping n -> p2 = f_mapping (S n) -> 
                                                            pc (offset + p1) = t1_loc.
unfold offset;unfold t1_loc;simpl;intros.
generalize (f_mapping_point_to_l0 n);intros.
generalize (NEXT_c (f_mapping n));rewrite H1;simpl;intuition.
generalize (NEXT_c (S (f_mapping n)));rewrite H13;simpl;intuition.
rewrite H;auto.
Qed.

Implicit Arguments offset_is_t1_loc [n p1 p2].

Lemma offset_is_less : forall n p1 p2, p1 = f_mapping n -> p2 = f_mapping (S n) -> 
                                                            offset  < p2 - p1.
intros.
unfold offset.
cut (p2 = 11 + p1);[omega|];intros.
apply (l0_between_l0_is_10 p1 p2);try rewrite H;try rewrite H0.
apply f_mapping_monotony;auto with arith.
apply f_mapping_point_to_l0.
apply f_mapping_point_to_l0.
apply f_mapping_no_l0_between.
Qed.

Implicit Arguments offset_is_less [n p1 p2].

Lemma t1_loc_is_unique : forall n p1 p2, p1 = f_mapping n -> p2 = f_mapping (S n) -> 
                                                            forall p, p1 <= p < p2 -> p <> offset + p1 -> pc p <> t1_loc.
intros.
assert (p2 = 11 + p1);intros.
apply (l0_between_l0_is_10 p1 p2);try rewrite H;try rewrite H0.
apply f_mapping_monotony;auto with arith.
apply f_mapping_point_to_l0.
apply f_mapping_point_to_l0.
apply f_mapping_no_l0_between.
rewrite H3 in *.
clear H3 p2 H0.
assert (p < p1 \/ p = p1 \/ p = 1 + p1 \/ p = 2 + p1 \/ p = 3 + p1 \/ p = 4 + p1 \/ p = 5 + p1 \/ p = 6 + p1 \/ p = 7 + p1\/ p = 8 + p1 \/ p = 9 + p1\/ p = 10 + p1 \/ 11 + p1 <= p).
omega.
generalize (f_mapping_point_to_l0 n);intros.
rewrite <- H in H3.
unfold offset in H2; unfold t1_loc;intuition.
rewrite H0 in H4.
rewrite H4 in H3;discriminate.
generalize (l0_add_1_l1 p1 H3 );rewrite <-H1;intro Hn;rewrite Hn in H4;discriminate.
generalize (l0_add_3_l3 p1 H3 );rewrite <-H1;intro Hn;rewrite Hn in H4;discriminate.
generalize (l0_add_4_l4 p1 H3 );rewrite <-H0;intro Hn;rewrite Hn in H4;discriminate.
generalize (l0_add_5_l5 p1 H3 );rewrite <-H1;intro Hn;rewrite Hn in H4;discriminate.
generalize (l0_add_6_l6 p1 H3 );rewrite <-H0;intro Hn;rewrite Hn in H4;discriminate.
generalize (l0_add_7_l7 p1 H3 );rewrite <-H1;intro Hn;rewrite Hn in H4;discriminate.
generalize (l0_add_8_l8 p1 H3 );rewrite <-H0;intro Hn;rewrite Hn in H4;discriminate.
generalize (l0_add_9_l9 p1 H3 );rewrite <-H1;intro Hn;rewrite Hn in H4;discriminate.
generalize (l0_add_10_l10 p1 H3 );rewrite <-H0;intro Hn;rewrite Hn in H4;discriminate.
Qed.

Implicit Arguments t1_loc_is_unique [n p1 p2].

(*in this hypothesis, m1 is used because of the concrete model. This can changed based on different concrete model*)
Lemma offset_change_property :  forall n p1 p2, p1 = f_mapping n -> p2 = f_mapping (S n) -> 
                                                            forall p, offset + p1 <= p < p2 -> m1 (S p) = m1 p.
intros.
assert (p2 = 11 + p1);intros.
apply (l0_between_l0_is_10 p1 p2);try rewrite H;try rewrite H0.
apply f_mapping_monotony;auto with arith.
apply f_mapping_point_to_l0.
apply f_mapping_point_to_l0.
apply f_mapping_no_l0_between.
rewrite H2 in *.
clear H0 p2 H2.
unfold offset in *.
assert (p < 2 + p1 \/ p = 2 + p1 \/ p = 3 + p1 \/ p = 4 + p1 \/ p = 5 + p1 \/ p = 6 + p1 \/ p = 7 + p1\/ p = 8 + p1 \/ p = 9 + p1\/ p = 10 + p1 \/ 11 + p1 <= p).
omega.
generalize (f_mapping_point_to_l0 n);intros.
rewrite <- H in H2.
intuition.
Show 2.
generalize (l0_add_2_l2 p1 H2 );intro Ht;rewrite <-H0 in Ht;generalize (NEXT_c p);rewrite Ht;simpl;tauto.
generalize (l0_add_3_l3 p1 H2 );intro Ht;rewrite <-H1 in Ht;generalize (NEXT_c p);rewrite Ht;simpl;tauto.
generalize (l0_add_4_l4 p1 H2 );intro Ht;rewrite <-H0 in Ht;generalize (NEXT_c p);rewrite Ht;simpl;tauto.
generalize (l0_add_5_l5 p1 H2 );intro Ht;rewrite <-H1 in Ht;generalize (NEXT_c p);rewrite Ht;simpl;tauto.
generalize (l0_add_6_l6 p1 H2 );intro Ht;rewrite <-H0 in Ht;generalize (NEXT_c p);rewrite Ht;simpl;tauto.
generalize (l0_add_7_l7 p1 H2 );intro Ht;rewrite <-H1 in Ht;generalize (NEXT_c p);rewrite Ht;simpl;tauto.
generalize (l0_add_8_l8 p1 H2 );intro Ht;rewrite <-H0 in Ht;generalize (NEXT_c p);rewrite Ht;simpl;tauto.
generalize (l0_add_9_l9 p1 H2 );intro Ht;rewrite <-H1 in Ht;generalize (NEXT_c p);rewrite Ht;simpl;tauto.
generalize (l0_add_10_l10 p1 H2 );intro Ht;rewrite <-H0 in Ht;generalize (NEXT_c p);rewrite Ht;simpl;tauto.
Qed.

Implicit Arguments offset_change_property [n p1 p2].

(*end of hypothesis need to be proved*)

(*this two lemmas are proved not using the information about the PLC program*)

Lemma l2_2_l0 : forall p, pc p = l2 -> pc (pred (pred p)) = l0.
intros.
generalize (f_mapping_between p);intros.
elim H0;intros.
assert ((f_mapping x <= p < f_mapping (S x)) \/ p = f_mapping (S x));intros.
elim_clear H1.
assert (p < f_mapping (S x) \/ p = f_mapping (S x));intros.
apply le_lt_or_eq;auto.
elim_clear H1.
left;omega.
right;auto.
clear H1.
elim_clear H2.
Focus 2.
rewrite H1 in H.
rewrite (f_mapping_point_to_l0 (S x)) in H;discriminate.
generalize (t1_loc_is_unique (refl_equal (f_mapping x)) (refl_equal (f_mapping (S x)))  _ H1);intros.
generalize (imply_to_or _ _  H2);intros.
unfold not in *.
elim_clear H3.
generalize (NNPP _ H4);intros.
rewrite H3;simpl.
apply (f_mapping_point_to_l0).
unfold t1_loc in *.
apply False_ind;auto.
Qed.

Lemma l2_lt_2 : forall p, pc p = l2 -> 2 <= p.
intros.
generalize (f_mapping_between p);intros.
elim H0;intros.
assert ((f_mapping x <= p < f_mapping (S x)) \/ p = f_mapping (S x));intros.
elim_clear H1.
assert (p < f_mapping (S x) \/ p = f_mapping (S x));intros.
apply le_lt_or_eq;auto.
elim_clear H1.
left;omega.
right;auto.
clear H1.
elim_clear H2.
Focus 2.
rewrite H1 in H.
rewrite (f_mapping_point_to_l0 (S x)) in H;discriminate.
generalize (t1_loc_is_unique (refl_equal (f_mapping x)) (refl_equal (f_mapping (S x)))  _ H1);intros.
generalize (imply_to_or _ _  H2);intros.
unfold not in *.
elim_clear H3.
generalize (NNPP _ H4);intros.
rewrite H3;simpl.
omega.
unfold t1_loc in *.
apply False_ind;auto.
Qed.

(*this hypothesis can be proved manually, but cannot be proved in Coq for now.*)
Lemma f_mapping_existence : forall p, pc p = l0 ->  exists n, f_mapping n = p.
intros.
generalize (f_mapping_between p);intros.
elim_clear H0.
assert (f_mapping x = p \/ f_mapping x < p < f_mapping (S x) \/ p = f_mapping (S x));intros.
elim_clear H1.
elim (le_lt_or_eq _ _ H0);intros;elim (le_lt_or_eq _ _ H2);intros;[right;left;omega|auto|auto|auto].
elim_clear H0.
exists x;auto.
elim_clear H2.
generalize (f_mapping_no_l0_between x _ _ H0);intros.
elim H2;auto.
exists (S x);auto.
Qed.


(*assumptions about the execution times of rungs. We only list the first 2 assumptions, since they are enough for our reasoning.*)

Hypothesis rung0_execution_time:
    forall p1 p2, pc p1 = l0 -> pc p2 = l0 -> fc (S p1) - fc p1 = fc (S p2) - fc p2.

Hypothesis rung1_execution_time:
    forall p1 p2, pc p1 = l1 -> pc p2 = l1 -> fc (S p1) - fc p1 = fc (S p2) - fc p2.

(*Lemmas about the interval relations*)

Lemma l0_l2_interval_same : 
    forall p1 p2, p1 < p2 -> pc p1 = l2 -> pc p2 = l2 -> fc p2 - fc p1 = fc (pred (pred p2)) - fc (pred (pred p1)).
intros.
cut (fc p2 - fc (pred (pred p2)) = fc p1 - fc (pred (pred p1))).
intros.
cut (fc (pred (pred p2)) < fc p2).
cut (fc (pred (pred p1)) < fc p1).
intros.
omega.
destruct p1.
generalize INIT_c; intro Hi; red in Hi; intuition.
rewrite H17 in H0;discriminate.
simpl.
cut (pc p1 = l1);intros.
destruct p1.
generalize INIT_c; intro Hi; red in Hi; intuition.
rewrite H18 in H3;discriminate.
simpl.
apply fc_monotonic_g;auto with arith.
generalize (before_l2_is_l1 (S p1));simpl;auto.
destruct p2.
generalize INIT_c; intro Hi; red in Hi; intuition.
simpl.
cut (pc p2 = l1);intros.
destruct p2.
generalize INIT_c; intro Hi; red in Hi; intuition.
rewrite H18 in H3;discriminate.
simpl.
apply fc_monotonic_g;auto with arith.
generalize (before_l2_is_l1 (S p2));simpl;auto.
generalize (l2_lt_2 _ H0);intros.
generalize (l2_lt_2 _ H1);intros.
destruct p1.
inversion H2.
simpl.
destruct p1.
inversion H2.
inversion H5.
destruct p2.
inversion H3.
simpl.
destruct p2.
inversion H3.
inversion H5.
simpl.
assert (fc (S (S p2)) - fc p2 = fc (S (S p2)) - fc (S p2) + (fc (S p2) - fc p2)).
cut (fc (S p2) < fc (S (S p2))).
cut (fc p2 < fc (S p2)).
omega.
apply fc_monotonic;auto.
apply fc_monotonic;auto.
assert (fc (S (S p1)) - fc p1 = fc (S (S p1)) - fc (S p1) + (fc (S p1) - fc p1)).
cut (fc (S p1) < fc (S (S p1))).
cut (fc p1 < fc (S p1)).
omega.
apply fc_monotonic;auto.
apply fc_monotonic;auto.
rewrite (rung0_execution_time p2 p1) in H4.
rewrite (rung1_execution_time (S p2) (S p1)) in H4.
rewrite H4.
rewrite H5.
auto.
generalize (before_l2_is_l1 (S (S p2)));simpl;auto.
generalize (before_l2_is_l1 (S (S p1)));simpl;auto.
assert (pc (S p2) = l1).
generalize (before_l2_is_l1 (S (S p2)));simpl;auto.
generalize (before_l1_is_l0 (S p2));simpl;auto.
assert (pc (S p1) = l1).
generalize (before_l2_is_l1 (S (S p1)));simpl;auto.
generalize (before_l1_is_l0 (S p1));simpl;auto.
Qed.


(*the correspond between the abstract model and the concrete model. And this corresponce can be used to prove some proproties.
The experiment shows that this corresponce is enough for the proof.*)

Lemma fc_all_lg_0 : forall c, 0 < fc (S c).
intros.
cut (fc 0 < fc (S c)).
  omega.
induction c.
 apply fc_monotonic.
generalize (fc_monotonic (S c)); intros;  omega.
Qed.

Lemma fc_1 :
    forall c1 c2, c1 < c2 -> fc c1 < fc c2.
intros.
induction H.
  eapply fc_monotonic.
cut (fc m < fc (S m)); intros.
  omega.
 eapply fc_monotonic.
Qed.

Lemma fc_1_le :
    forall c1 c2, c1 <= c2 -> fc c1 <= fc c2.
intros.
elim H; auto.
intros.
cut (fc m < fc (S m)); intros; try  omega.
apply fc_1; auto.
Qed.

Lemma fc_2 :
    forall c1 c2, fc c1 < fc c2 -> c1 < c2.
intros.
assert (c1 < c2 \/ c2 <= c1).
omega.
elim H0;intros;auto.
generalize (fc_1_le _ _ H1);intros.
omega.
Qed.

Section abstract_model_trace.

Definition t1_PT := t1_PT_c.
Hypothesis t1_LargerThan0 : 
    1 <= t1_PT.
Hypothesis t1_eq : t1_PT = t1_PT_c.
    
(*help functions*)
Definition being_true (v:Var) c1 c2 :=
                    forall c, c1 <= c <= c2 -> v c.
Definition being_false (v:Var) c1 c2 :=
                    forall c, c1 <= c <= c2 -> ~ v c.
                
Theorem Induction_lt: 
            forall P : nat -> Prop,
       (forall n : nat, (forall m : nat, m < n -> P m) -> P n) ->
       forall n : nat, P n.
intros P H n.
 eapply well_founded_induction_type.
   cut (well_founded lt).
    intros H0.
    apply H0.
   apply Wf_nat.lt_wf.
  auto.       
Qed.

(*a map from cycle to real time*)
Variable f : Cycle -> Time.
Hypothesis f_monotonic : forall c, f c < f (S c).

Lemma f_all_lg_0 : forall c, 0 < f (S c).
intros c.
cut (f 0 < f (S c)).
  omega.
induction c.
 apply f_monotonic.
generalize (f_monotonic (S c)); intros;  omega.
Qed.

Lemma f_1 :
    forall c1 c2, c1 < c2 -> f c1 < f c2.
intros c1 c2 H.
induction H.
  eapply f_monotonic.
cut (f m < f (S m)); intros.
  omega.
 eapply f_monotonic.
Qed.

Lemma f_1_le :
    forall c1 c2, c1 <= c2 -> f c1 <= f c2.
intros c1 c2 H.
elim H; auto.
intros.
cut (f m < f (S m)); intros; try  omega.
apply f_1; auto.
Qed.

Lemma f_2 :
    forall c1 c2, f c1 < f c2 -> c1 < c2.
intros.
cut (c1 < c2 \/ c2 <= c1);[|omega];intros.
elim H0;intros;auto.
generalize (f_1_le _ _ H1);intros;omega.
Qed.
    
Lemma f_3_inner_leftfix:
        forall c1 c2 c3 v, c1 <= c2 <= c3 -> f c3 - f c1 < v -> f c2 - f c1 < v.
intros c1 c2 c3 v H H0.
elim_clear H.
g_intro (f_1_le c2 c3 H2).
omega.
Qed.

Lemma f_3_inner_rightfix:
        forall c1 c2 c3 v, c1 <= c2 <= c3 -> f c3 - f c1 < v -> f c3 - f c2 < v.
intros.
elim_clear H.
g_intro (f_1_le c1 c2 H1).
omega.
Qed.

Lemma f_3_inner:
    forall c1 c2 c3 c4 v, c1<=c2 -> c2<=c3 -> c3 <= c4->
                f c4 - f c1 < v -> f c3 - f c2 < v.
intros.
g_intro (f_1_le c1 c2 H).
g_intro (f_1_le c3 c4 H1).
omega.
Qed.
    
Hypothesis f_TimerLargerThanCycleInterval :
                    forall c, f (S c) -  f c < t1_PT.  

(*
all the relays without timer
i0 - start
i1 - reset
i2 - player 1
i3 - player 2
i4 - player 3

m1 - running symbol
m2 - player 1
m3 - player 2
m4 - player 3
m5 - lock symbol if any one press the button

o0 - time out
o1 - player 1 pressed
o2 - player 2 pressed
o3 - player 3 pressed

*)
Variables i0 i1 i2 i3 i4 : Var.
Variables m1 m2 m3 m4 m5: Var.
Variables o0 o1 o2 o3 : Var.


(*the model of timer*)
Variable t1 : Var.


Definition initial_condition_a i0 i1 i2 i3 i4 m1 m2 m3 m4 m5 o0 o1 o2 o3 t1:=
    i0 = False /\ i1 = False /\ i2 = False /\ i3 = False /\ i4 = False /\
    m1 = False /\ m2 = False /\ m3 = False /\ m4 = False /\ m5 = False /\
    o0 = False /\ o1= False /\ o2 = False /\ o3= False /\
    t1 = False.

Check initial_condition_a.

Definition next_condition_a (i0 i1 i2 i3 i4 m1 m2 m3 m4 m5 o0 o1 o2 o3 t1 i0' i1' i2' i3' i4' m1' m2' m3' m4' m5' o0' o1' o2' o3' t1' : Prop) := 
    (m1' = ((i0' \/ m1) /\ ~ i1')) /\
    (m2' = (((~ t1' /\ i2' /\ ~ m5) \/ m2) /\ m1')) /\
    (m3' = (((~ t1' /\ i3' /\ ~ m5) \/ m3) /\ m1')) /\
    (m4' = (((~ t1' /\ i4' /\ ~ m5) \/ m4) /\ m1')) /\                                            
    (m5' = (((m2' \/ m3' \/ m4') \/ m5) /\ m1')) /\
    (o1' = m2') /\
    (o2' = m3') /\
    (o3' = m4') /\
    (o0' = (t1' /\ ~ m5')).

Print next_condition_a.

Hypothesis INIT_a : initial_condition_a  (i0 0) (i1 0) (i2 0) (i3 0) (i4 0) (m1 0) (m2 0) (m3 0) (m4 0) (m5 0) (o0 0) (o1 0) (o2 0) (o3 0) (t1 0).
Hypothesis NEXT_a : forall p, 
    next_condition_a (i0 p) (i1 p) (i2 p) (i3 p) (i4 p) (m1 p) (m2 p) (m3 p) (m4 p) (m5 p) (o0 p) (o1 p) (o2 p) (o3 p) (t1 p)
    (i0 (S p)) (i1 (S p)) (i2 (S p)) (i3 (S p)) (i4 (S p)) (m1 (S p)) (m2 (S p)) (m3 (S p)) (m4 (S p)) (m5 (S p)) (o0 (S p)) (o1 (S p)) (o2 (S p)) (o3 (S p)) (t1 (S p)).

Hypothesis h_t1_reset : forall c, ~ m1 c -> ~ t1 c. 

Hypothesis h_t1_set : 
        forall c1 c2, t1_PT <= f (pred c2) - f (pred c1) -> 
            being_true m1 c1 c2 -> t1 c2. 
            
Hypothesis h_t1_true :
        forall c2, t1 c2 -> exists c1, t1_PT <= f (pred c2) - f (pred c1) /\ being_true m1 c1 c2.

(*predicates about the struct of the PLC*)

Lemma h_m1 : forall c, m1 c = 
                                            ((i0 c \/ m1 (pred c)) 
                                            /\ ~ i1 c).
red in INIT_a;red in NEXT_a.
induction c.
intuition.
simpl.
rewrite H1.
rewrite H4.
rewrite H. 
apply my_proof_irrelevance_rl.
tauto.
apply my_proof_irrelevance_rl.
generalize (NEXT_a c).
intros [H1 [H2 [H3 [H4 [H5 [H6 [H7 [H8 H9]]]]]]]].
simpl in *.
rewrite H1.
split;auto.
Qed.

Lemma h_m2 : forall c, m2 c = 
                                            (((~ t1 c /\ i2 c /\ ~ m5 (pred c)) 
                                            \/ m2 (pred c)) 
                                            /\ m1 c).
red in INIT_a;red in NEXT_a.
induction c.
intuition.
simpl.
rewrite H0.
rewrite H8.
rewrite H5.
rewrite H4.
apply my_proof_irrelevance_rl;tauto.
apply my_proof_irrelevance_rl.
generalize (NEXT_a c).
intros [H1 [H2 [H3 [H4 [H5 [H6 [H7 [H8 H9]]]]]]]].
simpl in *.
rewrite H2.
split;auto.
Qed.

Lemma h_m3 : forall c, m3 c = 
                                            (((~ t1 c /\ i3 c /\ ~ m5 (pred c)) 
                                            \/ m3 (pred c)) 
                                            /\ m1 c).
red in INIT_a;red in NEXT_a.
induction c.
intuition.
simpl.
rewrite H2.
rewrite H6.
apply my_proof_irrelevance_rl;tauto.
apply my_proof_irrelevance_rl.
generalize (NEXT_a c).
intros [H1 [H2 [H3 [H4 [H5 [H6 [H7 [H8 H9]]]]]]]].
simpl in *.
rewrite H3.
split;auto.
Qed.
                                           
Lemma h_m4 : forall c, m4 c = 
                                            (((~ t1 c /\ i4 c /\ ~ m5 (pred c)) 
                                            \/ m4 (pred c)) 
                                            /\ m1 c).
red in INIT_a;red in NEXT_a.
induction c.
intuition.
simpl.
rewrite H3.
rewrite H7.
apply my_proof_irrelevance_rl;tauto.
apply my_proof_irrelevance_rl.
generalize (NEXT_a c).
intros [H1 [H2 [H3 [H4 [H5 [H6 [H7 [H8 H9]]]]]]]].
simpl in *.
rewrite H4.
split;auto.
Qed.
                                                                                        
Lemma h_m5 : forall c, m5 c =
                                            (((m2 c \/ m3 c \/ m4 c) 
                                            \/ m5 (pred c)) 
                                            /\ m1 c).
red in INIT_a;red in NEXT_a.
induction c.
intuition;simpl.
rewrite H8;rewrite H4.
apply my_proof_irrelevance_rl;tauto.
apply my_proof_irrelevance_rl.
generalize (NEXT_a c).
intros [H1 [H2 [H3 [H4 [H5 [H6 [H7 [H8 H9]]]]]]]].
simpl in *.
rewrite H5.
split;auto.
Qed.

Lemma h_o1 : forall c, o1 c = m2 c.
red in INIT_a;red in NEXT_a.
induction c.
intuition;simpl.
rewrite H10;rewrite H5.
apply my_proof_irrelevance_rl.
split;auto.
apply my_proof_irrelevance_rl.
generalize (NEXT_a c).
intros [H1 [H2 [H3 [H4 [H5 [H6 [H7 [H8 H9]]]]]]]].
rewrite H6.
split;auto.
Qed.

Lemma h_o2 : forall c, o2 c = m3 c.
red in INIT_a;red in NEXT_a.
induction c.
intuition;simpl.
rewrite H11;rewrite H6.
apply my_proof_irrelevance_rl.
split;auto.
apply my_proof_irrelevance_rl.
generalize (NEXT_a c).
intros [H1 [H2 [H3 [H4 [H5 [H6 [H7 [H8 H9]]]]]]]].
rewrite H7.
split;auto.
Qed.

Lemma h_o3 : forall c, o3 c = m4 c.
red in INIT_a;red in NEXT_a.
induction c.
intuition;simpl.
rewrite H12;rewrite H7.
apply my_proof_irrelevance_rl.
split;auto.
apply my_proof_irrelevance_rl.
generalize (NEXT_a c).
intros [H1 [H2 [H3 [H4 [H5 [H6 [H7 [H8 H9]]]]]]]].
rewrite H8.
split;auto.
Qed.

Lemma h_o0 : forall c, o0 c = 
                                            (t1 c /\ ~ m5 c).
red in INIT_a;red in NEXT_a.
induction c.
intuition;simpl.
rewrite H14;rewrite H9.
apply my_proof_irrelevance_rl.
tauto.
generalize (NEXT_a c).
intros [H1 [H2 [H3 [H4 [H5 [H6 [H7 [H8 H9]]]]]]]].
rewrite H9.
split;auto.
Qed.


(*properties*)

Lemma reset_no_start_m1 : 
    forall c1 c2, i1 c1 -> being_false i0 c1 c2 ->
        being_false m1 c1 c2. 
intros.
intro.
intro.
elim H1.
intro.
clear H1.
elim H2.
 intros.
   red in |- *; intros.
   generalize (h_m1 c1); intros.
   rewrite H4 in H3; intros.
   elim H3; auto.
intros.
  red in |- *; intros.
  generalize (h_m1 (S m)); intros.
  rewrite H6 in H5; intros.
  elim H5; intros.
  simpl in H7.
  elim H7; intros.
 red in H0.
   generalize (H0 (S m)); intros.
   elim H10.
   omega.
 auto.
apply H3.
 auto.
    omega.
auto.
Qed.    

Lemma reset_no_start_m2 : 
    forall c1 c2, i1 c1 -> being_false i0 c1 c2 -> 
        being_false m2 c1 c2.
intros.
intro; intros.
generalize reset_no_start_m1; intros.
cut (~ m1 c); intros.
 generalize (h_m2 c); intros.
   rewrite H4 in |- *; intro.
   elim H5; auto.
unfold being_false in H2.
   eapply H2.
   apply H.
  apply H0.
  auto.
Qed.        
    
Lemma reset_no_start_m3 : 
    forall c1 c2, i1 c1 -> being_false i0 c1 c2 -> 
        being_false m3 c1 c2.
intros.
intro; intros.
generalize reset_no_start_m1; intros.
cut (~ m1 c); intros.
 generalize (h_m3 c); intros.
   rewrite H4 in |- *; intro.
   elim H5; auto.
unfold being_false in H2.
   eapply H2.
   apply H.
  apply H0.
  auto.
Qed.            
        
Lemma reset_no_start_m4 : 
    forall c1 c2, i1 c1 -> being_false i0 c1 c2 -> 
        being_false m4 c1 c2.
intros.
intro; intros.
generalize reset_no_start_m1; intros.
cut (~ m1 c); intros.
 generalize (h_m4 c); intros.
   rewrite H4 in |- *; intro.
   elim H5; auto.
unfold being_false in H2.
   eapply H2.
   apply H.
  apply H0.
  auto.
Qed.            

Lemma reset_no_start_m5 : 
    forall c1 c2, i1 c1 -> being_false i0 c1 c2 -> 
        being_false m5 c1 c2.
intros.
intro; intros.
generalize reset_no_start_m1; intros.
cut (~ m1 c); intros.
 generalize (h_m5 c); intros.
   rewrite H4 in |- *; intro.
   elim H5; auto.
unfold being_false in H2.
   eapply H2.
   apply H.
  apply H0.
  auto.
Qed.    

Lemma noi2_nom2 : forall c, ~ m2 c -> ~ i2 (S c) -> ~ m2 (S c).
unfold not in |- *; intros.
generalize (h_m2 (S c)); intros.
rewrite H2 in H1; clear H2.
elim_clear H1.
elim_clear H2.
  tauto.
auto.
Qed.

Lemma noi3_nom3 : forall c, ~ m3 c -> ~ i3 (S c) -> ~ m3 (S c).
unfold not in |- *; intros.
generalize (h_m3 (S c)); intros.
rewrite H2 in H1; clear H2.
elim_clear H1.
elim_clear H2.
  tauto.
auto.
Qed.

Lemma noi4_nom4 : forall c, ~ m4 c -> ~ i4 (S c) -> ~ m4 (S c).
unfold not in |- *; intros.
generalize (h_m4 (S c)); intros.
rewrite H2 in H1; clear H2.
elim_clear H1.
elim_clear H2.
  tauto.
auto.
Qed.

Lemma reset_start_noi2_nom2 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3, c2 < c3 -> being_false i2 (S c2) c3 -> 
        being_false m2 (S c2) c3.   
intros.
intro.
intro.
generalize (reset_no_start_m2 c1 c2 H0 H1); intros.
elim H5.
intro.
elim H7.
 intros.
   apply noi2_nom2; auto.
intros.
  apply noi2_nom2; auto.
  apply H9.
   omega.
Qed.

Lemma reset_start_noi3_nom3 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3, c2 < c3 -> being_false i3 (S c2) c3 -> 
        being_false m3 (S c2) c3.   
intros.
intro.
intro.
generalize (reset_no_start_m3 c1 c2 H0 H1); intros.
elim H5.
intro.
elim H7.
 intros.
   apply noi3_nom3; auto.
intros.
  apply noi3_nom3; auto.
  apply H9.
   omega.
Qed.

Lemma reset_start_noi4_nom4 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3, c2 < c3 -> being_false i4 (S c2) c3 -> 
        being_false m4 (S c2) c3.   
intros.
intro.
intro.
generalize (reset_no_start_m4 c1 c2 H0 H1); intros.
elim H5.
intro.
elim H7.
 intros.
   apply noi4_nom4; auto.
intros.
  apply noi4_nom4; auto.
  apply H9.
   omega.
Qed.

Lemma reset_noi2_nom2 : 
    forall c1 c2, i1 c1 -> being_false i2 c1 c2 ->
        being_false m2 c1 c2.   
intros.
intro.
intro.
elim H1.
intro.
elim H2.
 intros.
   intro.
   generalize (h_m2 c1); intros.
   rewrite H5 in H4.
   elim_clear H4.
   generalize (h_m1 c1); intros.
   rewrite H4 in H7.
   elim_clear H7.
   auto.
intros.
  intro.
  generalize (h_m2 (S m)); intros.
  rewrite H7 in H6.
  elim_clear H6.
  elim_clear H8.
 elim_clear H6.
   elim_clear H10.
   red in H0.
   generalize (H0 (S m)); intros.
   apply H10.
   omega.
 auto.
simpl in H6.
  apply H4; try  omega.
  auto.
Qed.

Lemma reset_noi3_nom3 : 
    forall c1 c2, i1 c1 -> being_false i3 c1 c2 ->
        being_false m3 c1 c2.   
intros.
intro.
intro.
elim H1.
intro.
elim H2.
 intros.
   intro.
   generalize (h_m3 c1); intros.
   rewrite H5 in H4.
   elim_clear H4.
   generalize (h_m1 c1); intros.
   rewrite H4 in H7.
   elim_clear H7.
   auto.
intros.
  intro.
  generalize (h_m3 (S m)); intros.
  rewrite H7 in H6.
  elim_clear H6.
  elim_clear H8.
 elim_clear H6.
   elim_clear H10.
   red in H0.
   generalize (H0 (S m)); intros.
   apply H10.
   omega.
 auto.
simpl in H6.
  apply H4; try  omega.
  auto.
Qed.

Lemma reset_noi4_nom4 : 
    forall c1 c2, i1 c1 -> being_false i4 c1 c2 ->
        being_false m4 c1 c2.   
intros.
intro.
intro.
elim H1.
intro.
elim H2.
 intros.
   intro.
   generalize (h_m4 c1); intros.
   rewrite H5 in H4.
   elim_clear H4.
   generalize (h_m1 c1); intros.
   rewrite H4 in H7.
   elim_clear H7.
   auto.
intros.
  intro.
  generalize (h_m4 (S m)); intros.
  rewrite H7 in H6.
  elim_clear H6.
  elim_clear H8.
 elim_clear H6.
   elim_clear H10.
   red in H0.
   generalize (H0 (S m)); intros.
   apply H10.
   omega.
 auto.
simpl in H6.
  apply H4; try  omega.
  auto.
Qed.

Lemma reset_start_noreset_m1 :
    forall c1 c2, i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
            forall c3, being_false i1 (S c2) c3 ->
                being_true m1 (S c2) c3. 
intros.
intro.
intro.
elim H3.
intro.
elim H4; intros.
 generalize (h_m1 (S c2)); intros.
   rewrite H6 in |- *.
   split.
  auto.
 auto.
generalize (h_m1 (S m)); intros.
  rewrite H8 in |- *.
  split.
 right; simpl in |- *.
   apply H6;  omega.
auto.
Qed.

Lemma reset_start_time_t1_remain_false:
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            being_false t1 (S c2) c3.
intros.
intro.
intros.
red in |- *; intros.
generalize (h_t1_true _ H6); intros.
elim_clear H7.
elim_clear H8.
generalize (reset_no_start_m1 c1 c2 H0 H1); intros.
red in H8; red in H9; red in H8.
generalize (H9 c2); intros.
generalize (H8 c2); intros.
cut (x <= c2 <= c /\ c1 <= c2 <= c2); intros.
 elim H12; auto.
split;auto.
split.
Focus 2.
elim H5;omega.
   cut (x <= c2 \/ c2 < x); intros.
Focus 2.
omega.
    elim H12; intros; auto.
assert (f (pred c) - f (pred x) < t1_PT).
eapply  (f_3_inner c2 (pred x) (pred c) c3 t1_PT).
clear H H0 H1 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12.
try omega.
cut (f (pred x) < f (pred c));intros.
g_intro ( f_2 (pred x) (pred c) H14).
clear H H0 H1 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12 H13 H14.
omega.
clear H H0 H1 H4 H5 H6 H8 H9 H10 H11 H12 H13.
omega.
clear H H0 H1 H3 H4 H6 H7 H8 H9 H10 H11 H12 H13.
omega.
auto.
clear H H0 H1 H3 H4 H5 H6 H8 H9 H10 H11 H12 H13.
omega.
Qed.

Lemma reset_start_exceed_time_t1_m5_false_general : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            c2 < c3 ->
            being_false i2 (S c2) c3 ->
            being_false i3 (S c2) c3 ->
            being_false i4 (S c2) c3 ->
            being_false i1 (S c2) c3 ->
            ~ m5 c3.
intro.
intro.
intro.
intro.
intro.
intro.
intro.
intro.
elim H3; intros.
 rewrite (h_m5 (S c2)) in |- *; red in |- *; intros.
   elim_clear H8.
   elim_clear H9.
  elim_clear H8.
   generalize reset_start_noi2_nom2; intros.
     red in H8; red in H8;  eapply (H8 c1 c2); auto.
    elim_clear H9.
   generalize reset_start_noi3_nom3; intros.
     red in H9; red in H9;  eapply (H9 c1 c2); auto.
    generalize reset_start_noi4_nom4; intros.
    red in H9; red in H9;  eapply (H9 c1 c2); auto.
   simpl in *.
   rewrite (h_m5 c2) in H8.
   elim_clear H8.
   generalize reset_no_start_m1; intros.
   red in H8; red in H8;  eapply (H8 c1 c2 H0 H1 c2); auto.
  rewrite (h_m5 (S m)) in |- *; red in |- *; intros.
  elim_clear H10.
  elim_clear H11.
 elim_clear H10.
  generalize reset_start_noi2_nom2; intros.
    red in H10; red in H10;  eapply H10.
     apply H.
    auto.
    auto.
    auto.
    cut (c2 < S m); intros.
     apply H13.
     omega.
    auto.
    cut (S c2 <= S m <= S m); try  omega.
    intros.
    apply H13.
    auto.
   elim_clear H11.
  generalize reset_start_noi3_nom3; intros.
    red in H11; red in H11;  eapply H11.
     apply H.
    auto.
    auto.
    auto.
    cut (c2 < S m); intros; try  omega.
    apply H13.
    auto.
    cut (S c2 <= S m <= S m); intros; try  omega.
    apply H13.
    auto.
   generalize reset_start_noi4_nom4; intros.
   red in H11; red in H11;  eapply H11.
    apply H.
   auto.
   auto.
   auto.
   cut (c2 < S m); intros; try  omega.
   apply H13.
   auto.
   cut (S c2 <= S m <= S m); intros; try  omega.
   apply H13.
   auto.
  simpl in *.
  apply H5; try intro; intros.
 apply H6; try  omega.
apply H7; try  omega.
apply H8; try  omega.
apply H9; try  omega.
auto.
Qed.

Lemma reset_start_time_i2_m2 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            forall c, 
            S c2 <= c <= c3 ->
            being_false i2 (S c2) (pred c) ->
            being_false i3 (S c2) (pred c) ->
            being_false i4 (S c2) (pred c) ->
            i2 c -> 
            forall c4, c <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_true m2 c c4.
intros.
intro; intros.
elim H12.
intro.
elim H13; intros.
 rewrite (h_m2 c) in |- *; split.
  left; repeat split.
    generalize reset_start_time_t1_remain_false; intros.
    red in H15.
     eapply H15.
     apply H.
    auto.
    auto.
    auto.
    apply H3.
    auto.
    auto.
    auto.
    generalize reset_start_exceed_time_t1_m5_false_general; intros.
    cut (pred c = c2 \/ pred c <> c2); intros.
     elim H16; intros.
    rewrite H17 in |- *.
      generalize reset_no_start_m5; intros.
      red in H18.
       eapply H18.
       apply H0.
      apply H1.
      auto.
      eapply H15.
      apply H.
     auto.
     auto.
     auto.
      omega.
     auto.
     auto.
     auto.
     auto.
     red in |- *; intros.
     elim_clear H18.
      eapply H11.
      omega.
   omega.
   generalize reset_start_noreset_m1; intros.
   red in H15.
    eapply H15.
    apply H0.
   apply H1.
   auto.
   apply H11.
    omega.
  rewrite (h_m2 (S m)) in |- *; repeat split.
 simpl in |- *.
   right.
   apply H15.
    omega.
generalize reset_start_noreset_m1; intros.
  red in H17.
   eapply H17.
   apply H0.
  apply H1.
  auto.
  apply H11.
   omega.
Qed.

Lemma reset_start_time_i2_m5 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            forall c, 
            S c2 <= c <= c3 ->
            being_false i2 (S c2) (pred c) ->
            being_false i3 (S c2) (pred c) ->
            being_false i4 (S c2) (pred c) ->
            i2 c -> 
            forall c4, c <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_true m5 c c4.
intros.
cut (being_true m2 c c4); intros.
 intro.
   intros.
   rewrite (h_m5 c0) in |- *; try split.
  left.
    left.
    apply H12; auto.
 generalize reset_start_noreset_m1; intros.
   red in H14.
    eapply H14.
    apply H0.
   apply H1.
   auto.
   apply H11.
    omega.
   eapply reset_start_time_i2_m2.
   apply H.
  auto.
  auto.
  auto.
  apply H3.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
Qed.



Lemma reset_start_time_i2_o0 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            forall c, 
            S c2 <= c <= c3 ->
            being_false i2 (S c2) (pred c) ->
            being_false i3 (S c2) c ->
            being_false i4 (S c2) c ->
            i2 c -> 
            forall c4, c <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_false o0 (S c2) c4.
intros.
cut (being_false o0 (S c2) c /\ being_false o0 c c4); intros.
 elim_clear H12.
   intro; intros.
   red in H13; red in H14.
   cut (c0 < c \/ c <= c0); intros.
    elim H15; intros.
   apply H13.
      omega.
  apply H14;  omega.
  omega.
  split.
 intro; intros.
   rewrite (h_o0 c0) in |- *; red in |- *; intros.
   elim_clear H13.
   generalize reset_start_time_t1_remain_false; intros.
   red in H13; red in H13.
    eapply H13.
    apply H.
   auto.
   auto.
   auto.
   apply H3.
   auto.
   cut (S c2 <= c0 <= c3); intros.
    apply H16.
    omega.
   auto.
  intro; intros.
  rewrite (h_o0 c0) in |- *; red in |- *; intros.
  elim_clear H13.
  generalize reset_start_time_i2_m5; intros.
  red in H13.
  apply H15.
   eapply H13.
   apply H.
  auto.
  auto.
  auto.
  apply H3.
  auto.
  apply H5.
  auto.
  intro; intros.
  red in H7.
  apply H7;  omega.
  intro; intros; red in H8; apply H8;  omega.
  auto.
  apply H10.
  auto.
   omega.
Qed.

Lemma reset_start_time_i2_i3i4disabled : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            forall c, 
            S c2 <= c <= c3 ->
            being_false i2 (S c2) (pred c) ->
            being_false i3 (S c2) c ->
            being_false i4 (S c2) c ->
            i2 c -> 
            forall c4, c <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_true m2 c c4 /\ being_false m3 c c4 /\ being_false m4 c c4.
repeat split.
  eapply (reset_start_time_i2_m2 c1 c2 H H0 H1 H2 c3); auto.
  intro; intros.
    apply H7;  omega.
 intro; intros.
   apply H8;  omega.
intro; intros.
  elim H12; intro.
  elim H13; intros.
 rewrite (h_m3 c) in |- *; red in |- *; intros.
   elim_clear H15.
   elim_clear H16.
  elim_clear H15.
    elim_clear H18.
    red in H7; red in H7.
     eapply (H7 c); auto.
     omega.
 cut (S c2 = c \/ S c2 < c); intros.
  elim_clear H16.
   rewrite <- H18 in *; simpl in *.
     generalize reset_no_start_m3; intros.
     red in H16; red in H16.
      eapply H16.
      apply H0.
     apply H1.
     cut (c1 <= c2 <= c2); intros; try  omega.
     apply H19.
     auto.
    generalize reset_start_noi3_nom3; intros.
    red in H16; red in H16;  eapply H16.
     apply H.
    auto.
    auto.
    auto.
    cut (c2 < c); intros.
     apply H19.
    omega.
    auto.
    cut (S c2 <= pred c <= c); intros.
     apply H19.
     omega.
    auto.
    omega.
  rewrite (h_m3 (S m)) in |- *; red in |- *; intros; simpl in *.
  elim_clear H17.
  elim_clear H18.
 elim_clear H17.
   elim_clear H20.
   apply H21.
   generalize reset_start_time_i2_m5; intros.
   red in H20.
    eapply H20.
    apply H.
   auto.
   auto.
   auto.
   apply H3.
   auto.
   apply H5.
   auto.
   red in H7.
   intro; intros.
   apply H7.
    omega.
   red in H8.
   intro; intros.
   apply H8.
    omega.
   auto.
   apply H10.
   auto.
    omega.
  apply H15.
  omega.
auto.
  intro; intros.
  elim H12; intro.
  elim H13; intros.
 rewrite (h_m4 c) in |- *; red in |- *; intros.
   elim_clear H15.
   elim_clear H16.
  elim_clear H15.
    elim_clear H18.
    red in H8; red in H8.
     eapply (H8 c); auto.
     omega.
 cut (S c2 = c \/ S c2 < c); intros.
  elim_clear H16.
   rewrite <- H18 in *; simpl in *.
     generalize reset_no_start_m4; intros.
     red in H16; red in H16.
      eapply H16.
      apply H0.
     apply H1.
     cut (c1 <= c2 <= c2); intros; try  omega.
     apply H19.
     auto.
    generalize reset_start_noi4_nom4; intros.
    red in H16; red in H16;  eapply H16.
     apply H.
    auto.
    auto.
    auto.
    cut (c2 < c); intros.
     apply H19.
     omega.
    auto.
    cut (S c2 <= pred c <= c); intros.
     apply H19.
     omega.
    auto.
    omega.
  rewrite (h_m4 (S m)) in |- *; red in |- *; intros; simpl in *.
  elim_clear H17.
  elim_clear H18.
 elim_clear H17.
   elim_clear H20.
   apply H21.
   generalize reset_start_time_i2_m5; intros.
   red in H20.
    eapply H20.
    apply H.
   auto.
   auto.
   auto.
   apply H3.
   auto.
   apply H5.
   auto.
   red in H7.
   intro; intros.
   apply H7.
    omega.
   red in H8.
   intro; intros.
   apply H8.
    omega.
   auto.
   apply H10.
   auto.
    omega.
  apply H15.
  omega.
auto.
Qed.

Lemma reset_start_time_i2_m3m4 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            forall c, 
            S c2 <= c <= c3 ->
            being_false i2 (S c2) (pred c) ->
            being_false i3 (S c2) c ->
            being_false i4 (S c2) c ->
            i2 c -> 
            forall c4, c <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_true m2 c c4 /\ being_false m2 (S c2) (pred c) /\ being_false m3 (S c2) c4 /\ being_false m4 (S c2) c4.
intros.
generalize
 (reset_start_time_i2_i3i4disabled c1 c2 H H0 H1 H2 c3 H3 H4 c H5 H6 H7 H8 H9
    c4 H10 H11); intros.
elim_clear H12.
elim_clear H14.
repeat split.
 auto.
intro.
  intros.
  generalize reset_start_noi2_nom2; intros.
  red in H16.
   eapply H16.
   apply H.
  auto.
  auto.
  auto.
  cut (c2 < pred c); intros.
   apply H17.
   omega.
  auto.
  omega.
  assert (being_false m3 (S c2) c).
  eapply reset_start_noi3_nom3.
    apply H.
   auto.
   auto.
   auto.
    omega.
   auto.
  red in |- *; intros.
  cut (c0 < c \/ c <= c0); intros.
   elim_clear H17.
  red in H14.
    apply H14; auto.
     omega.
 red in H12.
   apply H12;  omega.
 omega.
  assert (being_false m4 (S c2) c).
 generalize reset_start_noi4_nom4; intros.
    eapply H14.
    apply H.
   auto.
   auto.
   auto.
    omega.
   auto.
  red in |- *; intros.
  cut (c0 < c \/ c <= c0); intros.
   elim_clear H17.
  red in H14.
    apply H14; auto.
     omega.
 red in H15.
   apply H15;  omega.
 omega.
Qed.





Lemma reset_start_time_i2_o0o1o2o3 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            forall c, 
            S c2 <= c <= c3 ->
            being_false i2 (S c2) (pred c) ->
            being_false i3 (S c2) c ->
            being_false i4 (S c2) c ->
            i2 c -> 
            forall c4, c <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_false o0 (S c2) c4 /\
                being_true o1 c c4 /\ 
                being_false o1 (S c2) (pred c) /\ 
                being_false o2 (S c2) c4 /\ 
                being_false o3 (S c2) c4.
intros.
split.
 generalize
  (reset_start_time_i2_o0 c1 c2 H H0 H1 H2 c3 H3 H4 c H5 H6 H7 H8 H9 c4 H10
     H11).
   auto.
generalize
 (reset_start_time_i2_m3m4 c1 c2 H H0 H1 H2 c3 H3 H4 c H5 H6 H7 H8 H9 c4 H10
    H11); intros.
  elim_clear H12.
  elim_clear H14.
  elim_clear H15.
  repeat split.
 red in |- *; intros.
   rewrite (h_o1 c0) in |- *.
   apply H13; auto.
red in |- *; intros.
  rewrite (h_o1 c0) in |- *; intros.
  apply H12; auto.
red in |- *; intros.
  rewrite (h_o2 c0) in |- *; intros.
  apply H14; auto.
red in |- *; intros.
  rewrite (h_o3 c0) in |- *; intros.
  apply H16; auto.
Qed.

Lemma reset_start_time_i3_m3 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            forall c, 
            S c2 <= c <= c3 ->
            being_false i2 (S c2) (pred c) ->
            being_false i3 (S c2) (pred c) ->
            being_false i4 (S c2) (pred c) ->
            i3 c -> 
            forall c4, c <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_true m3 c c4.
intros.
intro; intros.
elim H12.
intro.
elim H13; intros.
 rewrite (h_m3 c) in |- *; split.
  left; repeat split.
    generalize reset_start_time_t1_remain_false; intros.
    red in H15.
     eapply H15.
     apply H.
    auto.
    auto.
    auto.
    apply H3.
    auto.
    auto.
    auto.
    generalize reset_start_exceed_time_t1_m5_false_general; intros.
    cut (pred c = c2 \/ pred c <> c2); intros.
     elim H16; intros.
    rewrite H17 in |- *.
      generalize reset_no_start_m5; intros.
      red in H18.
       eapply H18.
       apply H0.
      apply H1.
      auto.
      eapply H15.
      apply H.
     auto.
     auto.
     auto.
      omega.
     auto.
     auto.
     auto.
     auto.
     red in |- *; intros.
     elim_clear H18.
      eapply H11.
      omega.
   omega.
   generalize reset_start_noreset_m1; intros.
   red in H15.
    eapply H15.
    apply H0.
   apply H1.
   auto.
   apply H11.
    omega.
  rewrite (h_m3 (S m)) in |- *; repeat split.
 simpl in |- *.
   right.
   apply H15.
    omega.
generalize reset_start_noreset_m1; intros.
  red in H17.
   eapply H17.
   apply H0.
  apply H1.
  auto.
  apply H11.
   omega.
Qed.

Lemma reset_start_time_m5enabled_i4disabled : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            forall c, 
            S c2 <= c <= c3 ->
            being_false i4 (S c2) c ->
            forall c4, c <= c4 -> 
                being_true m5 c c4 ->
                being_false i1 (S c2) c4 ->
                being_false m4 c c4.
intros.
cut (~ m4 c); intros.
 intro; intros.
   elim H11; intro.
   elim H12; intros.
  auto.
 rewrite (h_m4 (S m)) in |- *; simpl in |- *; red in |- *; intros.
   elim_clear H16.
   elim_clear H17.
    elim_clear H16.
    elim_clear H19.
    apply H20.
    apply H8;  omega.
 apply H14; auto.
    omega.
  cut (being_false m4 (S c2) c); intros.
 apply H10;  omega.
 eapply reset_start_noi4_nom4.
   apply H.
  auto.
  auto.
  auto.
   omega.
  auto.
Qed.

Lemma reset_start_time_i2i3_i4disabled : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            forall c, 
            S c2 <= c <= c3 ->
            being_false i2 (S c2) (pred c) ->
            being_false i3 (S c2) (pred c) ->
            being_false i4 (S c2) c ->
            i2 c -> 
            i3 c ->
            forall c4, c <= c4 -> 
                being_false i1 (S c2) c4 ->
                
                being_false m2 (S c2) (pred c) /\
                being_true m2 c c4 /\ 
                being_false m3 (S c2) (pred c) /\
                being_true m3 c c4 /\ 
                being_false m4 (S c2) c4.
repeat split.
 generalize reset_start_noi2_nom2; intros.
   intro; intros.
   red in H13.
    eapply H13.
    apply H.
   auto.
   auto.
   auto.
   cut (S c2 <= pred c); intros.
    red in |- *.
    apply H15.
    omega.
   auto.
   auto.
   eapply reset_start_time_i2_m2.
   apply H.
  auto.
  auto.
  auto.
  apply H3.
  auto.
  auto.
  auto.
  auto.
  intro; intros.
  apply H8; auto.
   omega.
  auto.
  auto.
  auto.
  generalize reset_start_noi3_nom3; intros.
  red in H13.
  intro; intros.
   eapply H13.
   apply H.
  auto.
  auto.
  auto.
  cut (S c2 <= pred c); intros.
   red in |- *.
   apply H15.
   omega.
  auto.
  auto.
  generalize reset_start_time_i3_m3; intros.
   eapply H13.
   apply H.
  auto.
  auto.
  auto.
  apply H3.
  auto.
  auto.
  auto.
  auto.
  intro; intros.
  apply H8; auto.
   omega.
  auto.
  auto.
  auto.
  cut (being_false m4 (S c2) c /\ being_false m4 c c4); intros.
 elim_clear H13.
   intro; intros.
   cut (c0 < c \/ c <= c0); intros.
  elim_clear H16.
   apply H14;  omega.
  apply H15;  omega.
  omega.
split.
 intro; intros.
   generalize reset_start_noi4_nom4; intros.
   red in H14.
    eapply H14.
    apply H.
   auto.
   auto.
   auto.
   cut (S c2 <= c); intros.
    red in |- *; apply H15.
    omega.
   auto.
    omega.
  generalize reset_start_time_m5enabled_i4disabled; intros.
  red in H13.
  intro; intros.
   eapply H13.
   apply H.
  auto.
  auto.
  auto.
  apply H3.
  auto.
  apply H5.
  auto.
  apply H11.
  auto.
  generalize reset_start_time_i2_m5; intros.
   eapply H15.
   apply H.
  auto.
  auto.
  auto.
  apply H3.
  auto.
  auto.
  auto.
  auto.
  intro; intros.
   eapply H8; auto.
   omega.
  auto.
  auto.
  auto.
  auto.
  auto.
Qed.

Lemma reset_start_time_i2i3_o0 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            forall c, 
            S c2 <= c <= c3 ->
            being_false i2 (S c2) (pred c) ->
            being_false i3 (S c2) (pred c) ->
            being_false i4 (S c2) c ->
            i2 c -> 
            i3 c ->
            forall c4, c <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_false o0 (S c2) c4.
intros.
intros.
cut (being_false o0 (S c2) c /\ being_false o0 c c4); intros.
 elim_clear H13.
   intro; intros.
   red in H14; red in H15.
   cut (c0 < c \/ c <= c0); intros.
  elim H16; intros.
   apply H14.
      omega.
  apply H15;  omega.
  omega.
split.
 intro; intros.
   rewrite (h_o0 c0) in |- *; red in |- *; intros.
   elim_clear H14.
   generalize reset_start_time_t1_remain_false; intros.
   red in H14; red in H14.
    eapply H14.
    apply H.
   auto.
   auto.
   auto.
   apply H3.
   auto.
   cut (S c2 <= c0 <= c3); intros.
    apply H17.
    omega.
   auto.
  intro; intros.
  rewrite (h_o0 c0) in |- *; red in |- *; intros.
  elim_clear H14.
  generalize reset_start_time_i2_m5; intros.
  red in H14.
  apply H16.
   eapply H14.
   apply H.
  auto.
  auto.
  auto.
  apply H3.
  auto.
  apply H5.
  auto.
  auto.
  red in |- *; intros; red in H8; apply H8;  omega.
  auto.
  apply H11.
  auto.
   omega.
Qed.

Lemma reset_start_time_i2i3_o0o1o2o3 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            forall c, 
            S c2 <= c <= c3 ->
            being_false i2 (S c2) (pred c) ->
            being_false i3 (S c2) (pred c) ->
            being_false i4 (S c2) c ->
            i2 c -> 
            i3 c ->
            forall c4, c <= c4 -> 
                being_false i1 (S c2) c4 ->
                
                being_false o0 (S c2) c4 /\
                being_true o1 c c4 /\ 
                being_false o1 (S c2) (pred c) /\ 
                being_true o2 c c4 /\ 
                being_false o2 (S c2) (pred c) /\ 
                being_false o3 (S c2) c4.
intros.
split.
  eapply reset_start_time_i2i3_o0.
    apply H.
   auto.
   auto.
   auto.
   apply H3.
   auto.
   apply H5.
   auto.
   auto.
   auto.
   auto.
   auto.
   auto.
   auto.
  generalize
   (reset_start_time_i2i3_i4disabled c1 c2 H H0 H1 H2 c3 H3 H4 c H5 H6 H7 H8
      H9 H10 c4 H11 H12); intros.
  elim_clear H13.
  elim_clear H15.
  elim_clear H16.
  elim_clear H17.
  repeat split.
 intro; intros.
   rewrite (h_o1 c0) in |- *; intros.
    eapply H13; auto.
intro; intros.
  rewrite (h_o1 c0) in |- *; intros.
   eapply H14; auto.
intro; intros.
  rewrite (h_o2 c0) in |- *; intros.
   eapply H16; auto.
intro; intros.
  rewrite (h_o2 c0) in |- *; intros.
   eapply H15; auto.
intro; intros.
  rewrite (h_o3 c0) in |- *; intros.
   eapply H18; auto.
Qed.

Lemma reset_start_exceed_time_t1 : 
    forall c1 c2, i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3, 
            t1_PT <= f (pred c3) - f c2 -> 
            being_false i1 (S c2) c3 ->
            t1 c3.  
intros.
intros.
cut (being_true m1 (S c2) c3); intros.
  eapply h_t1_set.
    cut (m1 (S c2)); intros.
cut (t1_PT <= f(pred c3) - f (pred (S c2)));intros.
apply H6.
simpl;auto.
    apply H4.
    split; auto.
    cut (f c2 < f (pred c3)); intros.
   generalize (f_2 c2 (pred c3)); intros.
      omega.
  cut (1 <= t1_PT); try  omega.

   auto.
  auto.
   eapply reset_start_noreset_m1.
   apply H.
  auto.
  auto.
  auto.
Qed.

Lemma reset_start_exceed_time_t1_strong : 
    forall c1 c2, i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            forall c4, S (S c3) <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_true t1 (S (S c3)) c4.    
intros.
intro; intros.
 eapply reset_start_exceed_time_t1.
   apply H.
  apply H0.
  auto.
  cut (f (S c3) <= f (pred c)); intros.
omega.
cut (S c3 = pred c \/ S c3 < pred c); intros; try  omega.
  elim H7; intros.
 rewrite H8 in |- *; auto.
cut (f (S c3) < f (pred c)); intros; try  omega.
  apply f_1; auto.
  intro; intros.
  apply H5.
   omega.
Qed.

Lemma reset_start_exceed_time_t1_m2_false_1 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            being_false i2 (S c2) (S (S c3)) ->
            forall c4, S (S c3) <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_false m2 (S (S c3)) c4.   
intros.
intro.
intro.
elim H8; intro.
elim H8; intro.
elim H9; intros.
 cut (~ m2 (S c3)); intros.
  rewrite (h_m2 (S (S c3))) in |- *; red in |- *; simpl in |- *; intros.
    elim_clear H14.
    elim_clear H15.
   elim_clear H14.
     elim_clear H17.
     cut (t1 (S (S c3))); auto.
      eapply reset_start_exceed_time_t1.
      apply H0.
     apply H1.
     auto.
     auto.
     auto.
     red in |- *; intros.
     apply H7;  omega.
    auto.
   generalize reset_start_noi2_nom2; intros.
   red in H13.
    eapply H13.
    apply H.
   auto.
   auto.
   auto.
   cut (c2 < (S c3)); intros.
    apply H14.
   cut (f c2 < f (S c3)); intros; try  omega.
   generalize (f_2 _ _ H14); intros; try  omega.
   intro.
   intros.
   apply H5.
   omega.
   split; auto.
   cut (c2 < S c3); try  omega.
   cut (f c2 < f (S c3)); intros; try  omega.
   generalize (f_2 _ _ H14); intros; try  omega.
  rewrite (h_m2 (S m)) in |- *; red in |- *; intros; simpl in *.
  elim_clear H15.
  elim_clear H16.
 cut (t1 (S m)); intros; try  tauto.
   generalize reset_start_exceed_time_t1_strong.
   intros.
   red in H16.
    eapply H16.
    apply H0.
   apply H1.
   auto.
   apply H3.
   auto.
   apply H6.
   auto.
   auto.
  apply H12; auto.
  omega.
 omega.
Qed.   
 
Lemma reset_start_exceed_time_t1_m2_false : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            being_false i2 (S c2) (S (S c3)) ->
            forall c4, S (S c3) <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_false m2 (S c2) c4.   
intros.
intros.
cut (being_false m2 (S c2) (S c3)); cut (being_false m2 (S (S c3)) c4); intros; auto.
 intro; intros.
   cut (S (S c3) <= c \/ S (S c3) > c); intros.
  elim H11; intros.
   apply H8; auto.
      omega.
  apply H9; try  omega.
  omega.
 eapply reset_start_exceed_time_t1_m2_false_1.
   apply H.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
   eapply reset_start_noi2_nom2.
   apply H.
  auto.
  auto.
  auto.
  cut (f c2 < f (S c3)); try  omega.
  intros.
  apply f_2; auto.
intro.
intros.
apply H5;omega.
   eapply reset_start_exceed_time_t1_m2_false_1.
   apply H.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
Qed.

Lemma reset_start_exceed_time_t1_m3_false_1 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            being_false i3 (S c2) (S (S c3)) ->
            forall c4, S (S c3) <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_false m3 (S (S c3)) c4.   
intros.
intro.
intro.
elim H8; intro.
elim H8; intro.
elim H9; intros.
 cut (~ m3 (S c3)); intros.
  rewrite (h_m3 (S (S c3))) in |- *; red in |- *; simpl in |- *; intros.
    elim_clear H14.
    elim_clear H15.
   elim_clear H14.
     elim_clear H17.
     cut (t1 (S (S c3))); auto.
      eapply reset_start_exceed_time_t1.
      apply H0.
     apply H1.
     auto.
     auto.
     auto.
     red in |- *; intros.
     apply H7;  omega.
    auto.
   generalize reset_start_noi3_nom3; intros.
   red in H13.
    eapply H13.
    apply H.
   auto.
   auto.
   auto.
   cut (c2 < (S c3)); intros.
    apply H14.
   cut (f c2 < f (S c3)); intros; try  omega.
   generalize (f_2 _ _ H14); intros; try  omega.
   intro.
   intros.
   apply H5.
   omega.
   split; auto.
   cut (c2 < S c3); try  omega.
   cut (f c2 < f (S c3)); intros; try  omega.
   generalize (f_2 _ _ H14); intros; try  omega.
  rewrite (h_m3 (S m)) in |- *; red in |- *; intros; simpl in *.
  elim_clear H15.
  elim_clear H16.
 cut (t1 (S m)); intros; try  tauto.
   generalize reset_start_exceed_time_t1_strong.
   intros.
   red in H16.
    eapply H16.
    apply H0.
   apply H1.
   auto.
   apply H3.
   auto.
   apply H6.
   auto.
   auto.
  apply H12; auto.
  omega.
 omega.
Qed.   
 
Lemma reset_start_exceed_time_t1_m3_false : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            being_false i3 (S c2) (S (S c3)) ->
            forall c4, S (S c3) <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_false m3 (S c2) c4.   
intros.
intros.
cut (being_false m3 (S c2) (S c3)); cut (being_false m3 (S (S c3)) c4); intros; auto.
 intro; intros.
   cut (S (S c3) <= c \/ S (S c3) > c); intros.
  elim H11; intros.
   apply H8; auto.
      omega.
  apply H9; try  omega.
  omega.
 eapply reset_start_exceed_time_t1_m3_false_1.
   apply H.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
   eapply reset_start_noi3_nom3.
   apply H.
  auto.
  auto.
  auto.
  cut (f c2 < f (S c3)); try  omega.
  intros.
  apply f_2; auto.
intro.
intros.
apply H5;omega.
   eapply reset_start_exceed_time_t1_m3_false_1.
   apply H.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
Qed.

Lemma reset_start_exceed_time_t1_m4_false_1 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            being_false i4 (S c2) (S (S c3)) ->
            forall c4, S (S c3) <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_false m4 (S (S c3)) c4.   
intros.
intro.
intro.
elim H8; intro.
elim H8; intro.
elim H9; intros.
 cut (~ m4 (S c3)); intros.
  rewrite (h_m4 (S (S c3))) in |- *; red in |- *; simpl in |- *; intros.
    elim_clear H14.
    elim_clear H15.
   elim_clear H14.
     elim_clear H17.
     cut (t1 (S (S c3))); auto.
      eapply reset_start_exceed_time_t1.
      apply H0.
     apply H1.
     auto.
     auto.
     auto.
     red in |- *; intros.
     apply H7;  omega.
    auto.
   generalize reset_start_noi4_nom4; intros.
   red in H13.
    eapply H13.
    apply H.
   auto.
   auto.
   auto.
   cut (c2 < (S c3)); intros.
    apply H14.
   cut (f c2 < f (S c3)); intros; try  omega.
   generalize (f_2 _ _ H14); intros; try  omega.
   intro.
   intros.
   apply H5.
   omega.
   split; auto.
   cut (c2 < S c3); try  omega.
   cut (f c2 < f (S c3)); intros; try  omega.
   generalize (f_2 _ _ H14); intros; try  omega.
  rewrite (h_m4 (S m)) in |- *; red in |- *; intros; simpl in *.
  elim_clear H15.
  elim_clear H16.
 cut (t1 (S m)); intros; try  tauto.
   generalize reset_start_exceed_time_t1_strong.
   intros.
   red in H16.
    eapply H16.
    apply H0.
   apply H1.
   auto.
   apply H3.
   auto.
   apply H6.
   auto.
   auto.
  apply H12; auto.
  omega.
 omega.
Qed.   
 
Lemma reset_start_exceed_time_t1_m4_false : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            being_false i4 (S c2) (S (S c3)) ->
            forall c4, S (S c3) <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_false m4 (S c2) c4.   
intros.
intros.
cut (being_false m4 (S c2) (S c3)); cut (being_false m4 (S (S c3)) c4); intros; auto.
 intro; intros.
   cut (S (S c3) <= c \/ S (S c3) > c); intros.
  elim H11; intros.
   apply H8; auto.
      omega.
  apply H9; try  omega.
  omega.
 eapply reset_start_exceed_time_t1_m4_false_1.
   apply H.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
   eapply reset_start_noi4_nom4.
   apply H.
  auto.
  auto.
  auto.
  cut (f c2 < f (S c3)); try  omega.
  intros.
  apply f_2; auto.
intro.
intros.
apply H5;omega.
   eapply reset_start_exceed_time_t1_m4_false_1.
   apply H.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
Qed.


Lemma reset_start_exceed_time_o123 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            being_false i2 (S c2) (S (S c3)) ->
            being_false i3 (S c2) (S (S c3)) ->
            being_false i4 (S c2) (S (S c3)) ->
            forall c4, S (S c3) <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_false o1 (S c2) c4 /\ being_false o2 (S c2) c4 /\ being_false o3 (S c2) c4.
repeat split.
 cut (being_false m2 (S c2) c4); intros.
  intro; intros.
    rewrite h_o1 in |- *; intros.
    apply H10; auto.
  eapply reset_start_exceed_time_t1_m2_false.
    apply H.
   auto.
   auto.
   auto.
   apply H3.
   auto.
   auto.
   auto.
   auto.
  cut (being_false m3 (S c2) c4); intros.
 intro; intros.
   rewrite h_o2 in |- *; intros.
   apply H10; auto.
 eapply reset_start_exceed_time_t1_m3_false.
   apply H.
  auto.
  auto.
  auto.
  apply H3.
  auto.
  auto.
  auto.
  auto.
  cut (being_false m4 (S c2) c4); intros.
 intro; intros.
   rewrite h_o3 in |- *; intros.
   apply H10; auto.
 eapply reset_start_exceed_time_t1_m4_false.
   apply H.
  auto.
  auto.
  auto.
  apply H3.
  auto.
  auto.
  auto.
  auto.
Qed.

Lemma reset_start_exceed_time_t1_m5_false : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            being_false i2 (S c2) (S (S c3)) ->
            being_false i3 (S c2) (S (S c3)) ->
            being_false i4 (S c2) (S (S c3)) ->
            forall c4, S (S c3) <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_false m5 (S c2) c4.   
intros.
cut
 (being_false m2 (S c2) c4 /\
  being_false m3 (S c2) c4 /\ being_false m4 (S c2) c4);
 intros.
 elim_clear H10.
   elim_clear H12.
   intro; intros.
   elim H12; intro.
   elim_clear H14.
  rewrite (h_m5 (S c2)) in |- *; red in |- *; intros.
    elim_clear H14.
    elim_clear H16.
   elim_clear H14.
    red in H11; red in H11.
       eapply H11; auto.
     elim_clear H16.
    red in H10; red in H10.
       eapply H10; auto.
     red in H13; red in H13.
      eapply H13; auto.
    simpl in *.
    generalize reset_no_start_m5; intros.
    red in H16; red in H16.
     eapply H16.
     apply H0.
    apply H1.
    cut (c1 <= c2 <= c2); intros.
     apply H18.
     omega.
    auto.
   rewrite (h_m5 (S m)) in |- *; red in |- *; intros.
   elim_clear H14.
   elim_clear H18.
  elim_clear H14.
   red in H11; red in H11.
      eapply H11; auto.
      cut (S c2 <= S m <= c4); intros; try  omega.
      apply H14.
     auto.
    elim_clear H18.
   red in H10; red in H10.
      eapply H10; auto.
      cut (S c2 <= S m <= c4); intros; try  omega.
      apply H18.
     auto.
    red in H13; red in H13.
     eapply H13; auto.
     cut (S c2 <= S m <= c4); intros; try  omega.
     apply H18.
    auto.
   simpl in H14.
   apply H16; try  omega; auto.
  repeat split.
  eapply reset_start_exceed_time_t1_m2_false.
    apply H.
   auto.
   auto.
   auto.
   apply H3.
   auto.
   auto.
   auto.
   auto.
   eapply reset_start_exceed_time_t1_m3_false.
   apply H.
  auto.
  apply H1.
  auto.
  apply H3.
  auto.
  auto.
  auto.
  auto.
   eapply reset_start_exceed_time_t1_m4_false.
   apply H.
  auto.
  auto.
  auto.
  apply H3.
  auto.
  auto.
  auto.
  auto.
Qed.

Lemma reset_start_time_t1_remain_false_strong:
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            being_false t1 (S c2) (S c3).
intros.
intro.
intros.
red in |- *; intros.
generalize (h_t1_true _ H6); intros.
elim_clear H7.
elim_clear H8.
generalize (reset_no_start_m1 c1 c2 H0 H1); intros.
red in H8; red in H9; red in H8.
generalize (H9 c2); intros.
generalize (H8 c2); intros.
cut (x <= c2 <= c /\ c1 <= c2 <= c2); intros.
 elim H12; auto.
split;auto.
split.
Focus 2.
elim H5;omega.
   cut (x <= c2 \/ c2 < x); intros.
Focus 2.
omega.
    elim H12; intros; auto.
assert (f (pred c) - f (pred x) < t1_PT).
eapply  (f_3_inner c2 (pred x) (pred c) c3 t1_PT).
clear H H0 H1 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12.
try omega.
cut (f (pred x) < f (pred c));intros.
g_intro ( f_2 (pred x) (pred c) H14).
clear H H0 H1 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12 H13 H14.
omega.
clear H H0 H1 H4 H5 H6 H8 H9 H10 H11 H12 H13.
omega.
clear H H0 H1 H3 H4 H6 H7 H8 H9 H10 H11 H12 H13.
omega.
auto.
clear H H0 H1 H3 H4 H5 H6 H8 H9 H10 H11 H12 H13.
omega.
Qed.


Lemma reset_start_exceed_time_o0o1o2o3 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            being_false i2 (S c2) (S (S c3)) ->
            being_false i3 (S c2) (S (S c3)) ->
            being_false i4 (S c2) (S (S c3)) ->
            forall c4, S (S c3) <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_false o0 (S c2) (S c3) /\ being_true o0 (S (S c3)) c4 /\
                being_false o1 (S c2) c4 /\ 
                being_false o2 (S c2) c4 /\ 
                being_false o3 (S c2) c4.
intros.
generalize
 (reset_start_exceed_time_o123 c1 c2 H H0 H1 H2 c3 H3 H4 H5 H6 H7 c4 H8 H9);
 intros.
elim_clear H10.
elim_clear H12.
repeat split; auto.
 red in |- *; intros.
   rewrite (h_o0 c) in |- *; red in |- *; intros.
   elim_clear H14.
   generalize reset_start_time_t1_remain_false_strong; intros.
   red in H14; red in H14.
    eapply H14.
    apply H.
   auto.
   auto.
   auto.
   apply H3.
   auto.
   apply H12.
   auto.
  red in |- *; intros.
  rewrite (h_o0 c) in |- *; intros.
  split.
 generalize reset_start_exceed_time_t1_strong; intros.
   red in H14.
    eapply H14.
    apply H0.
   apply H1.
   auto.
   apply H3.
   auto.
   apply H8.
   auto.
   auto.
  generalize reset_start_exceed_time_t1_m5_false; intros.
  red in H14.
   eapply H14.
   apply H.
  auto.
  auto.
  auto.
  apply H3.
  auto.
  auto.
  auto.
  auto.
  apply H8.
  auto.
  auto.
  cut (c2 < S c3); intros; try  omega.
  cut (f (c2) < f (S c3)); intros.
 apply f_2; auto.
 omega.         
Qed.


(*****************************************************************************)

(*final theorem for play press only*)

Definition reset_then_start c1 c2 := c1 <= c2 /\ i1 c1 /\ i0 (S c2) /\ being_false i0 c1 c2.
Definition just_time_out c1 c2 := t1_PT <= f (S c2) - f c1 /\ f c2 - f c1 < t1_PT. 
Definition p1_first_presses c1 c2 := being_false i2 c1 (pred c2) /\ being_false i3 c1 c2 /\ being_false i4 c1 c2 /\ i2 c2.
Definition p1p2_first_press c1 c2 := being_false i2 c1 (pred c2) /\ being_false i3 c1 (pred c2) /\ being_false i4 c1 c2 /\ i2 c2 /\ i3 c2.
Definition no_player_press c1 c2 := being_false i2 c1 c2 /\ being_false i3 c1 c2 /\ being_false i4 c1 c2.
Definition not_reset c1 c2 := being_false i1 c1 c2.
Definition off_on o c1 c2 c3 := being_true o c2 c3 /\ being_false o c1 (pred c2).
Definition stay_off o c1 c2 := being_false o c1 c2.


Theorem reset_start_time_i2_o0o1o2o3_f : 
    forall c1 c2, reset_then_start c1 c2 ->
        forall c3,
            just_time_out c2 c3 ->
            forall c, 
            S c2 <= c <= c3 -> p1_first_presses (S c2) c -> 
            forall c4, c <= c4 -> 
                not_reset (S c2) c4 ->
                stay_off o0 (S c2) c4 /\
                off_on o1 (S c2) c c4 /\
                stay_off o2 (S c2) c4 /\
                stay_off o3 (S c2) c4.
intros.
unfold stay_off in |- *; unfold off_on in |- *; unfold reset_then_start in *;
 unfold just_time_out in *; unfold p1_first_presses in *;
 unfold not_reset in *.
cut
 (being_false o0 (S c2) c4 /\
  being_true o1 c c4 /\
  being_false o1 (S c2) (pred c) /\
  being_false o2 (S c2) c4 /\ being_false o3 (S c2) c4);
 try  tauto.
elim_clear H.
elim_clear H6.
elim_clear H7.
elim_clear H0.
elim_clear H2.
elim_clear H10.
elim_clear H11.
 eapply (reset_start_time_i2_o0o1o2o3 c1 c2 H5 H H8 H6 c3);auto.
Qed.

(*final theorem for play 1 and player 2 press at exactly the same time*)

Theorem reset_start_time_i2i3_o0o1o2o3_f : 
    forall c1 c2, reset_then_start c1 c2 ->
        forall c3,
            just_time_out c2 c3 ->
            forall c, 
            S c2 <= c <= c3 ->
            p1p2_first_press (S c2) c ->
            forall c4, c <= c4 -> 
                not_reset (S c2) c4 ->
                stay_off o0 (S c2) c4 /\
                off_on o1 (S c2) c c4 /\
                off_on o2 (S c2) c c4 /\
                stay_off o3 (S c2) c4.
intros.
unfold stay_off in |- *; unfold off_on in |- *; unfold reset_then_start in *;
 unfold just_time_out in *; unfold p1_first_presses in *;
 unfold not_reset in *.
cut
 (being_false o0 (S c2) c4 /\
  being_true o1 c c4 /\
  being_false o1 (S c2) (pred c) /\
  being_true o2 c c4 /\
  being_false o2 (S c2) (pred c) /\ being_false o3 (S c2) c4);
 try  tauto.
elim_clear H.
elim_clear H6.
elim_clear H7.
elim_clear H0.
elim_clear H2.
elim_clear H10.
elim_clear H11.
elim_clear H12.
 eapply (reset_start_time_i2i3_o0o1o2o3 c1 c2 H5 H H8 H6 c3); auto.
Qed.


End abstract_model_trace.

Check reset_start_time_i2i3_o0o1o2o3_f.
Check reset_start_time_i2_o0o1o2o3_f .

(*relations between abstract and concrete initial and next conditions. What we want is they are enough to establish the properities.
First we give the axiom version. Then we prove the theorem version.
This relation can be proved or verified by a model checker. Also this can be done based on the HOARE logic, which is method used here manually.
*)

(*All the theorem here should be removed to the end of the abstract_model_trace section*)
Ltac g_intro_c H := generalize H;intros; clear H.

Theorem relation_con_abs : 
        forall p1 p2 , p1 < p2 -> pc p1 = l0 -> pc p2 = l0 -> (forall p, p1 < p < p2 -> pc p <> l0) -> 
            next_condition_a (i0 p1) (i1 p1) (i2 p1) (i3 p1) (i4 p1) (m1 p1) (m2 p1) (m3 p1) (m4 p1) (m5 p1) (o0 p1) (o1 p1) (o2 p1) (o3 p1) (t1 p1)
                    (i0 p2) (i1 p2) (i2 p2) (i3 p2) (i4 p2) (m1 p2) (m2 p2) (m3 p2) (m4 p2) (m5 p2) (o0 p2) (o1 p2) (o2 p2) (o3 p2) (t1 p2).
intros.
generalize (NEXT_c);intros.
unfold next_condition_a.
assert (p2 = 11 + p1).
apply l0_between_l0_is_10;auto.
rewrite H4 in *.
assert (pc (10 + p1) = l10).
elim (before_l0_is_l10_or_l0 (11+p1));intros.
simpl in *.
g_intro (l0_before_l0_0 (11 + p1)).
simpl in *.
g_intro (H6 H1 H5).
discriminate.
simpl in *;auto.
auto.
generalize (H3 (10+p1)).
unfold next_condition_c.
rewrite H5.
intros [eq0 [eq1 [eq2 [eq3 [eq4 [eq5 [eq6 [eq7 [eq8 [eq9 [eq10 [eq11 [eq12 [eq13 [eq14  eq_t]]]]]]]]]]]]]]].
simpl in *.
rewrite eq0.
rewrite eq1.
rewrite eq2.
rewrite eq3.
rewrite eq4.
rewrite eq5.
rewrite eq6.
rewrite eq7.
rewrite eq8.
rewrite eq9.
rewrite eq10.
rewrite eq11.
rewrite eq12.
rewrite eq13.
rewrite eq14.
clear eq0 eq1 eq2 eq3 eq4 eq5 eq6 eq7 eq8 eq9 eq10 eq11 eq12 eq13 eq14 eq_t.

assert (pc (9 + p1) = l9).
simpl in *.
g_intro (before_l10_is_l9 (10 + p1)).
simpl in *.
auto.
generalize (H3 (9+p1)).
unfold next_condition_c.
rewrite H6.
intros [eq0 [eq1 [eq2 [eq3 [eq4 [eq5 [eq6 [eq7 [eq8 [eq9 [eq10 [eq11 [eq12 [eq13 [eq14  eq_t]]]]]]]]]]]]]]].
simpl in *.
rewrite eq0.
rewrite eq1.
rewrite eq2.
rewrite eq3.
rewrite eq4.
rewrite eq5.
rewrite eq6.
rewrite eq7.
rewrite eq8.
rewrite eq9.
rewrite eq10.
rewrite eq12.
rewrite eq13.
rewrite eq14.
clear eq0 eq1 eq2 eq3 eq4 eq5 eq6 eq7 eq8 eq9 eq10 eq11 eq12 eq13 eq14 eq_t.

assert (pc (8 + p1) = l8).
simpl in *.
g_intro (before_l9_is_l8 (9 + p1)).
simpl in *.
auto.
generalize (H3 (8+p1)).
unfold next_condition_c.
rewrite H7.
intros [eq0 [eq1 [eq2 [eq3 [eq4 [eq5 [eq6 [eq7 [eq8 [eq9 [eq10 [eq11 [eq12 [eq13 [eq14  eq_t]]]]]]]]]]]]]]].
simpl in *.
rewrite eq0.
rewrite eq1.
rewrite eq2.
rewrite eq3.
rewrite eq4.
rewrite eq5.
rewrite eq6.
rewrite eq7.
rewrite eq8.
rewrite eq9.
rewrite eq10.
rewrite eq12.
rewrite eq14.
clear eq0 eq1 eq2 eq3 eq4 eq5 eq6 eq7 eq8 eq9 eq10 eq11 eq12 eq13 eq14 eq_t.

assert (pc (7 + p1) = l7).
simpl in *.
g_intro (before_l8_is_l7 (8 + p1)).
simpl in *.
auto.
generalize (H3 (7+p1)).
unfold next_condition_c.
rewrite H8.
intros [eq0 [eq1 [eq2 [eq3 [eq4 [eq5 [eq6 [eq7 [eq8 [eq9 [eq10 [eq11 [eq12 [eq13 [eq14  eq_t]]]]]]]]]]]]]]].
simpl in *.
rewrite eq0.
rewrite eq1.
rewrite eq2.
rewrite eq3.
rewrite eq4.
rewrite eq5.
rewrite eq6.
rewrite eq7.
rewrite eq8.
rewrite eq9.
rewrite eq10.
rewrite eq14.
clear eq0 eq1 eq2 eq3 eq4 eq5 eq6 eq7 eq8 eq9 eq10 eq11 eq12 eq13 eq14 eq_t.

assert (pc (6 + p1) = l6).
simpl in *.
g_intro (before_l7_is_l6 (7 + p1)).
simpl in *.
auto.
generalize (H3 (6+p1)).
unfold next_condition_c.
rewrite H9.
intros [eq0 [eq1 [eq2 [eq3 [eq4 [eq5 [eq6 [eq7 [eq8 [eq9 [eq10 [eq11 [eq12 [eq13 [eq14  eq_t]]]]]]]]]]]]]]].
simpl in *.
rewrite eq0.
rewrite eq1.
rewrite eq2.
rewrite eq3.
rewrite eq4.
rewrite eq5.
rewrite eq6.
rewrite eq7.
rewrite eq8.
rewrite eq9.
rewrite eq14.
clear eq0 eq1 eq2 eq3 eq4 eq5 eq6 eq7 eq8 eq9 eq10 eq11 eq12 eq13 eq14 eq_t.

assert (pc (5 + p1) = l5).
simpl in *.
g_intro (before_l6_is_l5 (6 + p1)).
simpl in *.
auto.
generalize (H3 (5+p1)).
unfold next_condition_c.
rewrite H10.
intros [eq0 [eq1 [eq2 [eq3 [eq4 [eq5 [eq6 [eq7 [eq8 [eq9 [eq10 [eq11 [eq12 [eq13 [eq14  eq_t]]]]]]]]]]]]]]].
simpl in *.
rewrite eq0.
rewrite eq1.
rewrite eq2.
rewrite eq3.
rewrite eq4.
rewrite eq5.
rewrite eq6.
rewrite eq7.
rewrite eq8.
rewrite eq9.
rewrite eq14.
clear eq0 eq1 eq2 eq3 eq4 eq5 eq6 eq7 eq8 eq9 eq10 eq11 eq12 eq13 eq14 eq_t.

assert (pc (4 + p1) = l4).
simpl in *.
g_intro (before_l5_is_l4 (5 + p1)).
simpl in *.
auto.
generalize (H3 (4+p1)).
unfold next_condition_c.
rewrite H11.
intros [eq0 [eq1 [eq2 [eq3 [eq4 [eq5 [eq6 [eq7 [eq8 [eq9 [eq10 [eq11 [eq12 [eq13 [eq14  eq_t]]]]]]]]]]]]]]].
simpl in *.
rewrite eq0.
rewrite eq1.
rewrite eq2.
rewrite eq3.
rewrite eq4.
rewrite eq5.
rewrite eq6.
rewrite eq7.
rewrite eq8.
rewrite eq9.
rewrite eq14.
clear eq0 eq1 eq2 eq3 eq4 eq5 eq6 eq7 eq8 eq9 eq10 eq11 eq12 eq13 eq14 eq_t.

assert (pc (3 + p1) = l3).
simpl in *.
g_intro (before_l4_is_l3 (4 + p1)).
simpl in *.
auto.
generalize (H3 (3+p1)).
unfold next_condition_c.
rewrite H12.
intros [eq0 [eq1 [eq2 [eq3 [eq4 [eq5 [eq6 [eq7 [eq8 [eq9 [eq10 [eq11 [eq12 [eq13 [eq14  eq_t]]]]]]]]]]]]]]].
simpl in *.
rewrite eq0.
rewrite eq1.
rewrite eq2.
rewrite eq3.
rewrite eq4.
rewrite eq5.
rewrite eq6.
rewrite eq7.
rewrite eq8.
rewrite eq9.
rewrite eq14.
clear eq0 eq1 eq2 eq3 eq4 eq5 eq6 eq7 eq8 eq9 eq10 eq11 eq12 eq13 eq14 eq_t.

assert (pc (2 + p1) = l2).
simpl in *.
g_intro (before_l3_is_l2 (3 + p1)).
simpl in *.
auto.
generalize (H3 (2+p1)).
unfold next_condition_c.
rewrite H13.
intros [eq0 [eq1 [eq2 [eq3 [eq4 [eq5 [eq6 [eq7 [eq8 [eq9 [eq10 [eq11 [eq12 [eq13   eq_t]]]]]]]]]]]]]].
simpl in *.
rewrite eq0.
rewrite eq1.
rewrite eq2.
rewrite eq3.
rewrite eq4.
rewrite eq5.
rewrite eq6.
rewrite eq7.
rewrite eq8.
rewrite eq9.
clear eq0 eq1 eq2 eq3 eq4 eq5 eq6 eq7 eq8 eq9 eq10 eq11 eq12 eq13 eq_t.

assert (pc (1 + p1) = l1).
simpl in *.
g_intro (before_l2_is_l1 (2 + p1)).
simpl in *.
auto.
generalize (H3 (1+p1)).
unfold next_condition_c.
rewrite H14.
intros [eq0 [eq1 [eq2 [eq3 [eq4 [eq5 [eq6 [eq7 [eq8 [eq9 [eq10 [eq11 [eq12 [eq13  [eq14 eq_t]]]]]]]]]]]]]]].
simpl in *.
rewrite eq0.
rewrite eq1.
rewrite eq2.
rewrite eq3.
rewrite eq4.
rewrite eq5.
rewrite eq6.
rewrite eq7.
rewrite eq8.
rewrite eq9.
clear eq0 eq1 eq2 eq3 eq4 eq5 eq6 eq7 eq8 eq9 eq10 eq11 eq12 eq13 eq14 eq_t.

generalize (H3 (p1)).
unfold next_condition_c.
rewrite H0.
intros [eq0 [eq1 [eq2 [eq3 [eq4 [eq5 [eq6 [eq7 [eq8 [eq9 eq_t]]]]]]]]]].
simpl in *.
rewrite eq0.
rewrite eq1.
rewrite eq2.
rewrite eq3.
rewrite eq4.
clear eq0 eq1 eq2 eq3 eq4 eq5 eq6 eq7 eq8 eq9 eq_t.

try repeat split;apply my_proof_irrelevance_rl;tauto.
Qed.

Theorem concrete_trace_sat_abs_init_condition:
    initial_condition_a  (abs i0 f_mapping 0) 
                                     (abs i1 f_mapping 0) 
                                     (abs i2 f_mapping 0) 
                                     (abs i3 f_mapping 0) 
                                     (abs i4 f_mapping 0)
                                     (abs m1 f_mapping 0) 
                                     (abs m2 f_mapping 0)
                                     (abs m3 f_mapping 0) 
                                     (abs m4 f_mapping 0) 
                                     (abs m5 f_mapping 0)
                                     (abs o0 f_mapping 0)
                                     (abs o1 f_mapping 0)
                                     (abs o2 f_mapping 0)
                                     (abs o3 f_mapping 0)
                                     (abs t1 f_mapping 0).
generalize (f_mapping_0_0);intros.
red;unfold abs;simpl.
rewrite H.
generalize (INIT_c);intros.
red in H0.
intuition.
Qed.

(*we can see that to prove the following theorem, the lemmes that are needed are only relation_con_abs and NEXT_c, which is an axiom here. So the only theorem is 
relation_con_abs that does matters. And at the same time, theorem relation_con_abs can be proved automatically by a automatic theorem prover. And this is the novel point
in this work.*)

Theorem concrete_trace_sat_abs_next_condition :
    forall p, next_condition_a       
                                     (abs i0 f_mapping p) 
                                     (abs i1 f_mapping p) 
                                     (abs i2 f_mapping p) 
                                     (abs i3 f_mapping p) 
                                     (abs i4 f_mapping p)
                                     (abs m1 f_mapping p) 
                                     (abs m2 f_mapping p)
                                     (abs m3 f_mapping p) 
                                     (abs m4 f_mapping p) 
                                     (abs m5 f_mapping p)
                                     (abs o0 f_mapping p)
                                     (abs o1 f_mapping p)
                                     (abs o2 f_mapping p)
                                     (abs o3 f_mapping p)
                                     (abs t1 f_mapping p)
                                     
                                     (abs i0 f_mapping (S p)) 
                                     (abs i1 f_mapping (S p)) 
                                     (abs i2 f_mapping (S p)) 
                                     (abs i3 f_mapping (S p)) 
                                     (abs i4 f_mapping (S p))
                                     (abs m1 f_mapping (S p)) 
                                     (abs m2 f_mapping (S p))
                                     (abs m3 f_mapping (S p)) 
                                     (abs m4 f_mapping (S p)) 
                                     (abs m5 f_mapping (S p))
                                     (abs o0 f_mapping (S p))
                                     (abs o1 f_mapping (S p))
                                     (abs o2 f_mapping (S p))
                                     (abs o3 f_mapping (S p))
                                     (abs t1 f_mapping (S p)).
intros.
unfold abs.
eapply relation_con_abs.
auto with base_f_mapping.
cut (pc (f_mapping p) = l0);intros.
apply H.
auto with base_f_mapping.
auto with base_f_mapping.
apply (f_mapping_no_l0_between ).
Qed.

Theorem equal_from_to : forall (v : Var_c) p1 p2, p1 <= p2 -> (forall p, p1 <= p < p2 -> v (S p) = v p) -> v p1 = v p2.
induction p1; induction p2;intros;auto.
rewrite H0.
apply IHp2.
auto with arith.
intros.
apply H0.
omega.
omega.
inversion H.
cut (p1 < p2 \/ p1 = p2);[|omega];intros.
elim H1;intros.
Focus 2.
rewrite H2;auto.
rewrite (H0 p2).
Focus 2.
omega.
apply IHp2.
auto with arith.
intros.
apply H0.
omega.
Qed.

Lemma t1_equal_offset_to_end : forall n p1 p2, p1 = f_mapping n -> p2 = f_mapping (S n) -> 
                                                            t1 (offset + 1+ p1) = t1 p2.
intros.
cut (forall p, offset + 1 + p1 <= p < p2 -> t1 (S p) = t1 p);intros.
apply equal_from_to.
generalize (offset_is_less (refl_equal (f_mapping n)) (refl_equal (f_mapping (S n))));intro.
omega.
auto.
apply (t1_loc_change_property (refl_equal (f_mapping n)) (refl_equal (f_mapping (S n)))).
omega.
apply (t1_loc_is_unique (refl_equal (f_mapping n)) (refl_equal (f_mapping (S n)))); omega.
Qed.

Implicit Arguments t1_equal_offset_to_end [n p1 p2].

Lemma m1_equal_offset_to_end : forall n p1 p2, p1 = f_mapping n -> p2 = f_mapping (S n) -> 
                                                            m1 (offset + p1) = m1 p2.
intros.
cut (forall p, offset + p1 <= p < p2 -> m1 (S p) = m1 p);intros.
apply equal_from_to.
generalize (offset_is_less (refl_equal (f_mapping n)) (refl_equal (f_mapping (S n))));intro.
omega.
auto.
apply (offset_change_property (refl_equal (f_mapping n)) (refl_equal (f_mapping (S n)))); omega.
Qed.

Implicit Arguments m1_equal_offset_to_end [n p1 p2].

(*
Hypothesis h_t1_reset_c : forall p, pc p = l2 -> ~ m1 p -> ~ t1 (S p).
*)

(*this theorem should be proved only used the hypothesis in the set h_set_1.*)
Theorem concrete_trace_sat_abs_t1_reset : forall c, ~ abs m1 f_mapping c -> ~ abs t1 f_mapping c. 
unfold abs.
destruct c.
rewrite (f_mapping_0_0).
generalize (INIT_c);intro Hi;red in Hi;intuition.
rewrite <- H17;auto.
generalize (t1_equal_offset_to_end (refl_equal (f_mapping c)) (refl_equal (f_mapping (S c))));intro.
generalize (m1_equal_offset_to_end (refl_equal (f_mapping c)) (refl_equal (f_mapping (S c))));intro.
rewrite <- H.
rewrite <- H0.
simpl.
apply h_t1_reset_c.
generalize (offset_is_t1_loc (refl_equal (f_mapping c)) (refl_equal (f_mapping (S c))));intros.
simpl in *.
auto.
Qed.

(*
Hypothesis h_t1_true_c : forall p2, pc (pred p2) = l2 -> t1 p2 -> 
                                                                exists p1, pc p1 = l2 /\ t1_PT_c <= fc (pred p2) - fc p1 /\
                                                                                  being_true_c m1 p1 (pred p2) l2 pc.
*)
          
Lemma concrete_trace_sat_abs_t1_true :
        forall c2, abs t1 f_mapping c2 -> exists c1, t1_PT <= abs fc f_mapping (pred c2) - abs fc f_mapping (pred c1) /\ being_true (abs m1 f_mapping) c1 c2.
unfold abs.
destruct c2.
intros.
rewrite (f_mapping_0_0) in H.
generalize (INIT_c);intro;red in H0;intuition.
rewrite H16 in H.
apply False_ind;auto.
intros.
simpl.
generalize (concrete_trace_sat_abs_t1_reset (S c2));unfold abs;simpl;intro.
assert (m1 (f_mapping (S c2))).
generalize (imply_to_or _ _ H0);intros.
elim H1;try tauto.
apply NNPP.
clear H0.
generalize (t1_equal_offset_to_end (refl_equal (f_mapping c2)) (refl_equal (f_mapping (S c2))));simpl;intro.
generalize H;intro.
rewrite <- H0 in H2.
clear H0.
generalize (offset_is_t1_loc (refl_equal (f_mapping c2)) (refl_equal (f_mapping (S c2))));simpl;unfold t1_loc;intro.
generalize (h_t1_true_c (S (S (S (f_mapping c2)))));simpl;intro.
generalize (H3 H0 H2);intro.
clear H3.
elim H4;clear H4.
intros p1;intros.
intuition.
generalize (l2_2_l0 _ H4);intros.
elim (f_mapping_existence _ H5);intro c1;intros.
exists (S c1);simpl.
split.
rewrite H7.
generalize (l0_l2_interval_same (p1) (S (S (f_mapping c2))));simpl;intros.
rewrite <- H8;unfold t1_PT;auto.
cut (S (S (f_mapping c1)) = p1);intros.
generalize (t1_PT_c_gt_zero);intros.
rewrite <-H9.
rewrite <- H9 in H3.
cut (fc (S (S (f_mapping c1))) < fc (S (S (f_mapping c2))));intros.
apply fc_monotonic_gr;auto.
omega.
generalize (l2_lt_2 _ H4);intros;omega.
intro;intros.
destruct c.
inversion H8.
inversion H9.
rewrite <- (m1_equal_offset_to_end (refl_equal (f_mapping c)) (refl_equal (f_mapping (S c)))).
apply H6.
Focus 2.
apply (offset_is_t1_loc (refl_equal (f_mapping c)) (refl_equal (f_mapping (S c)))).
generalize (l2_lt_2 _ H4);intros.
cut (S (S (f_mapping c1)) = p1);[intros|omega].
rewrite <- H10.
simpl.
cut (f_mapping c1 <= f_mapping c <= f_mapping c2);[omega|].
split;apply f_mapping_le;omega.
Qed.

(*
Hypothesis h_t1_set_c : forall p1 p2, pc p1 = l2 -> pc p2 = l2 -> 
                                                                t1_PT_c <= fc p2 - fc p1 ->
                                                                being_true_c m1 p1 p2 l2 pc ->
                                                                t1 (S p2). 

Hypothesis h_t1_set : 
        forall c1 c2, t1_PT <= f (pred c2) - f (pred c1) -> 
            being_true m1 c1 c2 -> t1 c2. 
*)

Theorem concrete_trace_sat_abs_t1_set : forall c1 c2, t1_PT <= abs fc f_mapping (pred c2) - abs fc f_mapping (pred c1) -> 
                                                                                         being_true (abs m1 f_mapping) c1 c2 -> abs t1 f_mapping c2.
unfold abs;intros. 
destruct c2.
simpl in H.
rewrite (f_mapping_0_0) in *.
generalize (t1_PT_c_gt_zero);intros.
unfold t1_PT in H.
apply False_ind;clear H0.
destruct (f_mapping (pred c1));[omega|generalize (fc_monotonic_g 0 (S p) );omega].
rewrite <- (t1_equal_offset_to_end (refl_equal (f_mapping c2)) (refl_equal (f_mapping (S c2))));intros.
simpl in *.
generalize offset_is_t1_loc;simpl;unfold t1_loc;intros.

apply (h_t1_set_c (S (S (f_mapping (pred c1)))) (S (S (f_mapping (c2)))));intros. 
apply (H1 (pred c1) (f_mapping (pred c1)) (f_mapping (S (pred c1))) (refl_equal (f_mapping (pred c1))) (refl_equal (f_mapping (S(pred c1))))).
apply (H1 (c2) (f_mapping (c2)) (f_mapping (S (c2))) (refl_equal (f_mapping (c2))) (refl_equal (f_mapping (S(c2))))).
unfold t1_PT in H.
rewrite l0_l2_interval_same;auto.
generalize (t1_PT_c_gt_zero);intros.
cut (f_mapping (pred c1) < f_mapping c2);auto with arith.
apply (fc_monotonic_gr);omega.
generalize (offset_is_t1_loc (refl_equal (f_mapping (pred c1))) (refl_equal (f_mapping (S (pred c1)))));simpl;unfold t1_loc;intro;auto.
generalize (offset_is_t1_loc (refl_equal (f_mapping (c2))) (refl_equal (f_mapping (S (c2)))));simpl;unfold t1_loc;intro;auto.
red;intros.
red in H0.
generalize (l2_2_l0 _ H3);intros.
generalize (f_mapping_existence _ H4);intros.
elim_clear H5.
assert (f_mapping (pred c1) <= pred (pred p) <= f_mapping c2);intros.
clear H6 H1 H0 H3 H H4.
omega.
rewrite <-H6 in H5.
assert (pred c1 <= x <= c2);intros.
elim H5;intros.
split;apply f_mapping_gr;auto.
cut (c1 <= S x <= S c2);[|clear H H0 H1 H2 H3 H4 H6 H5;omega];intros.
generalize (m1_equal_offset_to_end (sym_eq H6) (refl_equal (f_mapping(S x))));simpl;intros.
assert (S (S (pred (pred p))) = p);intros.
clear H H0 H1 H3 H4 H5 H6 H7 H8 H9;omega.
rewrite H10 in H9.
rewrite H9.
apply H0.
apply H8.
Qed.


Check concrete_trace_sat_abs_t1_reset.
Check concrete_trace_sat_abs_t1_true.
Check concrete_trace_sat_abs_t1_set.

Check reset_start_time_i2i3_o0o1o2o3_f.
Check reset_start_time_i2_o0o1o2o3_f .


Theorem con_reset_start_time_i2_o0o1o2o3_f :
forall c1 c2 : nat,
reset_then_start (abs i0 f_mapping) (abs i1 f_mapping) c1 c2 ->
forall c3 : nat,
just_time_out (abs fc f_mapping) c2 c3 ->
forall c : nat,
S c2 <= c <= c3 ->
p1_first_presses (abs i2 f_mapping) (abs i3 f_mapping) (abs i4  f_mapping) (S c2) c ->
forall c4 : nat,
c <= c4 ->
not_reset (abs i1 f_mapping)  (S c2) c4 ->
stay_off (abs o0 f_mapping)  (S c2) c4 /\
off_on (abs o1  f_mapping) (S c2) c c4 /\
stay_off (abs o2  f_mapping) (S c2) c4 /\ stay_off (abs o3 f_mapping)  (S c2) c4.
intros.
eapply reset_start_time_i2_o0o1o2o3_f.
unfold t1_PT.
apply (t1_PT_c_gt_zero).
intros.
cut (abs fc f_mapping c0 < abs fc f_mapping (S c0));intros.
apply H5.
unfold abs.
apply fc_monotonic_g.
apply f_mapping_monotony;auto with arith.
apply concrete_trace_sat_abs_init_condition. (*init condition*)
apply concrete_trace_sat_abs_next_condition. (*next state condition*)
apply concrete_trace_sat_abs_t1_true. (*timer 2*)
apply H.
apply H0.
auto.
auto.
auto.
auto.
Qed.


Theorem con_reset_start_time_i2i3_o0o1o2o3_f :
forall c1 c2 : nat,
reset_then_start (abs i0 f_mapping) (abs i1 f_mapping) c1 c2 ->
forall c3 : nat,
just_time_out (abs fc f_mapping) c2 c3 ->
forall c : nat,
S c2 <= c <= c3 ->
p1p2_first_press (abs i2 f_mapping) (abs i3 f_mapping) (abs i4 f_mapping) (S c2) c ->
forall c4 : nat,
c <= c4 ->
not_reset (abs i1 f_mapping) (S c2) c4 ->
stay_off (abs o0 f_mapping) (S c2) c4 /\
off_on (abs o1 f_mapping) (S c2) c c4 /\
off_on (abs o2 f_mapping) (S c2) c c4 /\ stay_off (abs o3 f_mapping) (S c2) c4.
intros.
eapply reset_start_time_i2i3_o0o1o2o3_f.
unfold t1_PT.
apply (t1_PT_c_gt_zero).
intros.
cut (abs fc f_mapping c0 < abs fc f_mapping (S c0));intros.
apply H5.
unfold abs.
apply fc_monotonic_g.
apply f_mapping_monotony;auto with arith.
apply concrete_trace_sat_abs_init_condition. (*init condition*)
apply concrete_trace_sat_abs_next_condition. (*next state condition*)
apply concrete_trace_sat_abs_t1_true. (*timer 2*)
apply H.
apply H0.
auto.
auto.
auto.
auto.
Qed.


*)
(*END -- All the theorem here should be removed to the end of the abstract_model_trace section*)


